proposition: Lemma CReq_not_apart : forall x y : CR, (x == y)%CR <-> (CRapartT x y -> False).
proof: Proof. split. - intros. destruct H0. revert c. apply CRle_not_lt. rewrite H. apply CRle_refl. revert c. apply CRle_not_lt. rewrite H. apply CRle_refl. - intros. apply CRle_antisym. split. apply CRle_not_lt. intro abs. contradict H. right. exact abs. apply CRle_not_lt. intro abs. contradict H. left. exact abs. 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