proposition: Lemma R_recip_as_IR : forall y Hy, (RasIR (1 / y) [=] ([1] [/] RasIR y [//] Hy)).
proof: Proof. intros y Hy. simpl in Hy. assert (y [#] 0). apply: R_ap_as_IR. stepr ([0]:IR). assumption. symmetry. apply R_Zero_as_IR. change (1/y) with ([1] [/] y [//] X). eapply eq_transitive. unfold RasIR. apply (map_pres_inv_unfolded RReals IR). apply div_wd; reflexivity. 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)