proposition: Lemma AReq_nlt : forall a b : AR, msp_eq a b <-> (fun x y : AR => (fun x0 y0 : AR => (ARltS y0 x0) -> False) y x /\ (fun x0 y0 : AR => (ARltS y0 x0) -> False) x y) a b.
proof: Proof. split. - split. pose proof (ARle_not_lt b a) as [H6 _]. apply H6. rewrite H5. apply PreOrder_Reflexive. pose proof (ARle_not_lt a b) as [H6 _]. apply H6. rewrite H5. apply PreOrder_Reflexive. - intros [J J0]. apply po_antisym. pose proof (ARle_not_lt a b) as [_ H6]. apply (H6 J0). pose proof (ARle_not_lt b a) as [_ H6]. apply (H6 J). Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.reals.faster.ARArith CoRN.reals.faster.ARabs CoRN.metric2.Metric CoRN.metric2.Complete CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs ConstructiveFastReals