proposition: Lemma AR_plus_lt_rev : ∀ r r1 r2 : AR, ARltS (ARplus r r1) (ARplus r r2) → ARltS r1 r2.
proof: Proof. intros. destruct (ARtoCR_preserves_ltT r1 r2) as [_ a]. apply a. clear a. pose proof (ARtoCR_preserves_plus r r1). pose proof (ARtoCR_preserves_plus r r2). destruct (ARtoCR_preserves_ltT (ARplus r r1) (ARplus r r2)) as [a _]. apply a in H5. clear a. apply (CRltT_wd H6 H7) in H5. pose proof (CRplus_lt_l ('r1) ('r2) ('r)) as [_ H8]. apply H8, H5. 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