I often find myself writing a definition which requires a proof. You are defining a term and, contextually, need to prove that the definition makes sense.

How can you express that? What about a definition with a proof?

Sometime one can write the definition and then the theorem. But often happens that many definition which should stay together need to be split because a theorem is required in between.

A tentative example:

**Definition** (rational numbers)
Let $\sim$ be the equivalence relation on $\mathbb Z^*\times \mathbb Z$ given
by
$$
(q,p) \sim (q',p') \iff pq' = p'q.
$$
We define $\mathbb Q= (\mathbb Z^*\times \mathbb Z)/\sim$.
On $\mathbb Q$ we define addition and multiplication as follows
$$
[(q,p)] + [(q',p')] = [(qq',pq'+p'q)] \\
[(q,p)] \cdot[(q',p')] = [(qq',pp')]
$$
With these operations and choosing
$0_\mathbb Q=[(1,0)]$, and $1_\mathbb Q=[(1,1)]$
turns out that $\mathbb Q$ is a field.

**Proof.**
We are going to prove that $\sim$ is indeed an equivalence relation,
that addition and multiplication are well defined and that the resulting
set is a field. [...]