proposition: Lemma Z_to_Qpositive_equal : forall (m1 m2 : Z) (Hm1 : (0 < m1)%Z) (Hm2 : (0 < m2)%Z), m1 = m2 -> Z_to_Qpositive m1 Hm1 = Z_to_Qpositive m2 Hm2.
proof: Proof. intros m1; induction m1. discriminate Hm1. unfold Z_to_Qpositive. intros m2 H Hm2 H_eq;revert Hm2. rewrite <- H_eq;reflexivity. intros m2 m1 abs;discriminate. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)