proposition: Lemma AR_ring : ring_theory (inject_Q_AR 0) (inject_Q_AR 1) ARplus ARmult (λ x y : AR, ARplus x (ARopp y)) ARopp (λ x y : AR, (λ x0 y0 : AR, ARltS y0 x0 → False) y x ∧ (λ x0 y0 : AR, ARltS y0 x0 → False) x y).
proof: Proof. destruct (rings.stdlib_ring_theory AR). split. - intros. apply AReq_nlt. rewrite AR_zero. apply (Radd_0_l x). - intros. apply AReq_nlt. apply (Radd_comm x y). - intros. apply AReq_nlt. apply (Radd_assoc x y z). - intros. apply AReq_nlt. rewrite AR_one. apply (Rmul_1_l x). - intros. apply AReq_nlt. apply (Rmul_comm x y). - intros. apply AReq_nlt. apply (Rmul_assoc x y z). - intros. apply AReq_nlt. apply (Rdistr_l x y z). - intros. apply AReq_nlt. reflexivity. - intros. apply AReq_nlt. rewrite AR_zero. apply (Ropp_def x). 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