proposition: Lemma CReq_nlt : forall a b : CR, msp_eq a b <-> (fun x y : CR => (fun x0 y0 : CR => (y0 < x0)%CR -> False) y x /\ (fun x0 y0 : CR => (y0 < x0)%CR -> False) x y) a b.
proof: Proof. split. - split. intro abs. exact (CRlt_irrefl _ (@CRltT_wd _ _ H b _ (reflexivity _) abs)). intro abs. exact (CRlt_irrefl _ (@CRltT_wd b _ (reflexivity _) _ _ H abs)). - intros [H H0]. apply CRle_antisym. split. apply CRle_not_lt in H0. exact H0. apply CRle_not_lt in H. exact H. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon