proposition: Lemma CRlt_irrefl (x: CR): x < x -> False.
proof: Proof. Proof with auto. unfold CRltT. intro. assert (x - x == 0)%CR by ring. intros. generalize (CRpos_wd H0 H). unfold CRpos. intros. destruct H1. destruct x0. simpl in c. assert (x0 <= 0)%Q. rewrite <- CRle_Qle... apply Qlt_irrefl with 0%Q. apply Qlt_le_trans with x0... Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders