proposition: Lemma AR_ring_ext : ring_eq_ext ARplus ARmult ARopp (λ x y : AR, (λ x0 y0 : AR, ARltS y0 x0 → False) y x ∧ (λ x0 y0 : AR, ARltS y0 x0 → False) x y).
proof: Proof. split. - intros x y J z t J0. apply AReq_nlt. apply AReq_nlt in J. apply AReq_nlt in J0. rewrite J, J0. reflexivity. - intros x y J z t J0. apply AReq_nlt. apply AReq_nlt in J. apply AReq_nlt in J0. rewrite J, J0. reflexivity. - intros x y J. apply AReq_nlt. apply AReq_nlt in J. rewrite J. reflexivity. 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