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