proposition: Lemma coding : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z), positive_fraction_encoding m n Hm Hn = spec_positive_fraction_encoding m n Hm Hn.
proof: Proof. intros m n Hm Hn. transitivity (Qpositive_c (S (pred_nat m Hm)) (S (pred_nat n Hn)) (S (pred_nat m Hm) + S (pred_nat n Hn))). unfold positive_fraction_encoding in |- *. generalize (Zminus2_wf m n Hm Hn); intro f. generalize Hm Hn; clear Hm Hn. pattern m, n, f in |- *. elim f using fractionalAcc_ind_dep; clear m n f; intros. rewrite (encoding_algorithm_0 m n Hm Hn (fractionalacc0 m n e) e). generalize Hm Hn. rewrite e. intros. symmetry in |- *. apply Qpositive_c_equal_One. apply f_equal with nat. apply pred_nat_equal. generalize (Zlt_minus n m l0). intro Hmn. rewrite (encoding_algorithm_1 m n Hm Hn (fractionalacc1 m n l l0 f) l0 l Hmn f) . rewrite plus_Sn_m. rewrite Qpositive_c_dL. apply f_equal with Qpositive. rewrite minus_pred_nat with n m Hn Hm Hmn. rewrite Qpositive_c_equal with (p' := S (pred_nat m Hm) + S (pred_nat (n - m) Hmn)); try auto with arith. rewrite (encoding_algorithm_equal m (n - m) l Hm Hmn Hmn f f). apply H. repeat rewrite absolu_pred_nat. replace (pred_nat m Hm) with (Z.abs_nat (m - 1)). repeat rewrite <- absolu_plus; try abstract lia. rewrite pred_nat_absolu; reflexivity. repeat rewrite absolu_pred_nat. apply lt_absolu; try abstract lia. generalize (Zlt_minus m n l0). intro Hmn. rewrite (encoding_algorithm_2 m n Hm Hn (fractionalacc2 m n l l0 f) l0 Hmn l f) . rewrite plus_Sn_m. rewrite Qpositive_c_nR. apply f_equal with Qpositive. rewrite minus_pred_nat with m n Hm Hn Hmn. rewrite Qpositive_c_equal with (p' := S (pred_nat (m - n) Hmn) + S (pred_nat n Hn)); try auto with arith. rewrite (encoding_algorithm_equal (m - n) n Hmn Hmn l Hn f f). apply H. repeat rewrite absolu_pred_nat. replace (pred_nat m Hm) with (Z.abs_nat (m - 1)). repeat rewrite <- absolu_plus; try abstract lia. rewrite pred_nat_absolu; reflexivity. repeat rewrite absolu_pred_nat. apply lt_absolu; try abstract lia. rewrite spec_positive_fraction_encoding1_positive_fraction_encoding. transitivity (spec_positive_fraction_encoding1 (S (pred_nat m Hm)) (S (pred_nat n Hn))). repeat rewrite Znat.inj_S. unfold Z.succ in |- *. apply spec_coding. repeat rewrite <- pred_nat_unfolded. reflexivity. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)