proposition: Lemma R_Q2R_as_IR : forall q, RasIR (Q2R q) [=] inj_Q IR q.
proof: Proof. intro q. destruct q. unfold Q2R. cut (Dom (f_rcpcl' IR) (RasIR (nring (R:=RRing) (nat_of_P Qden)))). intro Hy. stepr (RasIR (zring (R:=RRing) Qnum)[/]RasIR (nring (R:=RRing) (nat_of_P Qden))[//]Hy). stepl (RasIR (zring (R:=RRing) Qnum / nring (R:=RRing) (nat_of_P Qden))). apply (R_div_as_IR (zring Qnum) (nring (nat_of_P Qden))). apply R_as_IR_wd. unfold Rdiv. replace (nring (R:=RRing) (nat_of_P Qden)) with (INR (nat_of_P Qden)). replace (zring (R:=RRing) Qnum) with (IZR Qnum). now rewrite <- positive_nat_Z, INR_IZR_INZ. apply IZR_as_zring. apply INR_as_nring. apply div_wd. apply R_zring_as_IR. apply R_nring_as_IR. simpl. stepr (RasIR 0); [| now apply R_Zero_as_IR]. apply IR_ap_as_R. apply Rgt_not_eq. unfold Rgt. replace 0 with (nring (R:=RRing) 0). change ((nring (R:=RRing) 0 [<] nring (R:=RRing) (nat_of_P Qden))). apply nring_less. auto with *. auto with *. Qed.
imports: Coq.QArith.QArith Coq.QArith.Qreals Coq.QArith.QArith_base CoRN.tactics.CornTac Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun CoRN.coq_reals.Rreals CoRN.reals.iso_CReals CoRN.reals.CauchySeq Coq.Reals.Rtrigo_def CoRN.transc.PowerSeries Coq.Logic.ConstructiveEpsilon Coq.Reals.Rlogic Coq.Reals.Reals CoRN.transc.Pi CoRN.transc.MoreArcTan CoRN.logic.PropDecid CoRN.transc.Exponential Coq(Lia Lra)