proposition: Lemma CRlt_Qlt : forall a b, (a < b)%Q -> ((' a%Q) < (' b))%CR.
proof: Proof. intros a b H. destruct (Qpos_sub _ _ H) as [c Hc]. exists c. intros d. change (-proj1_sig d <= b + - a + - proj1_sig c). rewrite -> Hc. rewrite -> Qle_minus_iff. ring_simplify. apply Qpos_nonneg. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRFieldOps CoRN.model.ordfields.CRordfield CoRN.reals.CReals CoRN.reals.fast.CRcorrect CoRN.model.metric2.Qmetric CoRN.tactics.CornTac