proposition: Lemma spec_coding : forall m n : nat, Qpositive_c (S m) (S n) (S m + S n) = spec_positive_fraction_encoding1 (m + 1) (n + 1).
proof: Proof. unfold spec_positive_fraction_encoding1 in |- *. unfold Qmult in |- *. intros m n. transitivity (Qpositive_mult (Qpositive_c (S m) 1 (S (S m))) (Qpositive_inv (Qpositive_c (S n) 1 (S (S n))))). unfold Qpositive_mult in |- *. rewrite Qpositive_i_c; [ idtac | apply Nat.lt_0_succ | apply le_n ]. set (P := Qpositive_i (Qpositive_c (S n) 1 (S (S n)))) in *. set (p := fst P) in *. set (q := snd P) in *. transitivity (Qpositive_c (S m * 1) (1 * S n) (S m * 1 + 1 * S n)). repeat rewrite Nat.mul_1_l; repeat rewrite Nat.mul_1_r; reflexivity. assert (P = (S n, 1)). unfold P in |- *. apply Qpositive_i_c; try apply Nat.lt_0_succ. apply le_n. replace (Qpositive_i (Qpositive_inv (Qpositive_c (S n) 1 (S (S n))))) with (q, p). replace q with 1. replace p with (S n). reflexivity. change (S n = fst P) in |- *. rewrite H. reflexivity. change (1 = snd P) in |- *. rewrite H. reflexivity. symmetry in |- *. apply inv_correct. transitivity P. reflexivity. unfold p, q in |- *. apply pair_1. replace (m + 1)%Z with (Z.succ m); [ idtac | reflexivity ]. rewrite <- Znat.inj_S. replace (n + 1)%Z with (Z.succ n); [ idtac | reflexivity ]. rewrite <- Znat.inj_S. simpl in |- *. repeat rewrite nat_of_P_o_P_of_succ_nat_eq_succ. reflexivity. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)