proposition: Lemma IR_le_as_R_back : forall x y, (IRasR x <= IRasR y -> x [<=] y).
proof: Proof. intros. rewrite -> leEq_def. intro xy. cut (~ (IRasR y < IRasR x)); intro. apply H0. apply R_lt_as_IR. stepl y; [| now rewrite -> IRasRasIR_id; reflexivity]. stepr x; [| now rewrite -> IRasRasIR_id; reflexivity]. assumption . apply (RIneq.Rle_not_lt (IRasR y) (IRasR x)). assumption. assumption. 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)