proposition: Lemma spec_positive_fraction_encoding1_positive_fraction_encoding : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z), spec_positive_fraction_encoding m n Hm Hn = spec_positive_fraction_encoding1 m n.
proof: Proof. intros; unfold spec_positive_fraction_encoding, spec_positive_fraction_encoding1 in |- *; elim (inject_nat_S_inf m Hm); elim (inject_nat_S_inf n Hn); intros nn Hnn mm Hmm; generalize Hn Hm; rewrite Hnn; rewrite Hmm; intros; unfold Qmult in |- *; simpl in |- *; repeat rewrite nat_of_P_o_P_of_succ_nat_eq_succ; reflexivity. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)