proposition: Lemma spec_positive_fraction_encoding1_positive_fraction_encoding2 : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z), spec_positive_fraction_encoding m n Hm Hn = spec_positive_fraction_encoding2 m n.
proof: Proof. intros m n Hm Hn; unfold spec_positive_fraction_encoding2, spec_positive_fraction_encoding in |- *; apply f_equal2 with Qpositive Qpositive; try apply f_equal with Qpositive; destruct m as [| pm| pm]; try discriminate Hm; destruct n as [| pn| pn]; try discriminate Hn; reflexivity. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)