proposition: Lemma Z_to_Qpositive_to_Q : forall (m : Z) (Hm : (0 < m)%Z), Z_to_Q m = Qpos (Z_to_Qpositive m Hm).
proof: Proof. intros m; functional induction (Z_to_Q m); intros Hm; discriminate Hm || trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)