proposition: Lemma Qpositive_i_c : forall m p : nat, 0 < m -> S m <= p -> Qpositive_i (Qpositive_c m 1 p) = (m, 1).
proof: Proof. intros m p. generalize m; clear m. induction p. intros m H1 H2. inversion H2. intros m H1 H2. case (le_lt_eq_dec 1 m). auto with arith. intro H_1_m. rewrite (Qpositive_c_nR _ _ p H_1_m). rewrite (Qpositive_i_nR (Qpositive_c (m - 1) 1 p) (m - 1) 1). apply pair_2; simpl in |- *; trivial; lia. apply IHp; lia. intro H_1_1. rewrite <- H_1_1. reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)