proposition: Lemma CRlt_strext : Crel_strext CRasCField CRltT.
proof: Proof. intros x1 x2 y1 y2 H. destruct (Ccsr_strext _ _ _ (CRasCauchy_IR x2) _ (CRasCauchy_IR y2) (CR_lt_as_Cauchy_IR_lt_1 _ _ H)) as[H0|H0]. left. apply CR_lt_as_Cauchy_IR_lt_2. assumption. right. destruct H0;[left|right]; apply CR_ap_as_Cauchy_IR_ap_2; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRFieldOps CoRN.model.fields.CRfield CoRN.algebra.COrdFields CoRN.reals.fast.CRcorrect CoRN.tactics.CornTac