proposition: Lemma R_abs_as_IR : forall x, RasIR (Rabs x) [=] AbsIR (RasIR x).
proof: Proof. intro x. unfold Rabs. destruct (Rcase_abs x) as [Hx | Hx]. cut (RasIR x[<=][0]). intro Hxn. rewrite -> (AbsIR_eq_inv_x (RasIR x) Hxn). autorewrite with RtoIR; reflexivity. stepr (RasIR 0); [| now apply R_Zero_as_IR]. apply less_leEq. apply IR_lt_as_R. assumption. cut ([0] [<=] RasIR x). intro Hxn. rewrite -> (AbsIR_eq_x _ Hxn). reflexivity. stepl (RasIR 0); [| now apply R_Zero_as_IR]. apply IR_le_as_R. lra. 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)