proposition: Lemma CR_less_as_IR : forall x y, (IRasCR x < IRasCR y -> x[<]y)%CR.
proof: Proof. intros x y H. stepl (CRasIR (IRasCR x)); [| now apply IRasCRasIR_id]. stepr (CRasIR (IRasCR y)); [| now apply IRasCRasIR_id]. apply map_pres_less. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.CauchySeq CoRN.reals.iso_CReals CoRN.reals.R_morphism CoRN.reals.fast.CRArith CoRN.model.reals.CRreal CoRN.tactics.CornTac