proposition: Lemma Z_to_Q_to_R_IZR: forall z, Q_to_R (Z_to_Q z) = IZR z.
proof: Proof. intros [|p|p]. simpl; rewrite <- Q_to_R_Zero; trivial. unfold Z_to_Q, Q_to_R, numerator, denominator, decode_Q, fst, snd. rewrite (Qpositive_i_c (nat_of_P p) (S (nat_of_P p)) (lt_O_nat_of_P _)); trivial; repeat rewrite <- INR_IZR_INZ; unfold IZR, INR at 2; rewrite <- INR_IPR; field; auto. unfold Z_to_Q, Q_to_R, numerator, denominator, decode_Q, fst, snd. rewrite (Qpositive_i_c (nat_of_P p) (S (nat_of_P p)) (lt_O_nat_of_P _)); trivial. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ; unfold IZR, INR at 2; rewrite <- INR_IPR; field; auto. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)