proposition: Lemma ARlt_or_epsilon : forall a b c d : AR, ARlt a b \/ ARlt c d -> ARltS a b + ARltS c d.
proof: Proof. intros. destruct (CRlt_or_epsilon (cast AR CR a) (cast AR CR b) (cast AR CR c) (cast AR CR d)). - destruct H5. left. apply CR_lt_ltT, (ARtoCR_preserves_ltT a b), AR_lt_ltT. exact H5. right. apply CR_lt_ltT, (ARtoCR_preserves_ltT c d), AR_lt_ltT. exact H5. - left. apply (ARtoCR_preserves_ltT a b). exact c0. - right. apply (ARtoCR_preserves_ltT c d). exact c0. 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