proposition: Lemma Cauchy_IR_lt_as_CR_lt_1 : forall (x y:Cauchy_IR), x[<]y -> (Cauchy_IRasCR x < Cauchy_IRasCR y)%CR.
proof: Proof. intros x y [n [e He Hn]]. exists (exist _ _ He). abstract ( autorewrite with CRtoCauchy_IR; intros [m [d Hd Hm]]; refine (Qle_not_lt _ _ (Hn (Nat.max n m) _) _);[auto with *|]; rewrite -> Qlt_minus_iff; apply Qlt_le_trans with d;[assumption|]; autorewrite with QposElim in Hm; eapply Hm; auto with * ). Defined.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps