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. [...]