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