proposition: Lemma Qpositive_to_Z_is_integer_part : forall x : positive, Qpositive_to_Z (Qpositive_c (nat_of_P x) 1 (S (nat_of_P x))) = Zpos x.
proof: Proof. intro p. generalize (lt_O_nat_of_P p). rewrite <- ZL9. generalize (nat_of_P p). induction n; intro H. inversion H. apply Nat.le_succ_l in H. case (le_lt_eq_dec 1 (S n) H). intro H1. rewrite (Qpositive_c_nR _ _ (S n) H1). transitivity (1 + Qpositive_to_Z (Qpositive_c (S n - 1) 1 (S n)))%Z. reflexivity. rewrite Znat.inj_S. rewrite Z.add_comm. unfold Z.succ in |- *. apply f_equal2 with Z Z; trivial. rewrite <- IHn. apply f_equal with Qpositive. apply f_equal3 with nat nat nat; trivial. simpl in |- *; auto with arith. lia. intro H1; rewrite <- H1. rewrite Qpositive_c_equal_One; trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)