proposition: Lemma ARmult_inv_r : (∀ (r : AR) (rnz : (ARltS r (inject_Q_AR 0) + ARltS (inject_Q_AR 0) r)%type), (λ x y : AR, (λ x0 y0 : AR, ARltS y0 x0 → False) y x ∧ (λ x0 y0 : AR, ARltS y0 x0 → False) x y) (ARmult (ARinvS r rnz) r) (inject_Q_AR 1)).
proof: Proof. intros. rewrite <- AReq_nlt. rewrite (commutativity _ r). unfold ARinvS. pose proof (AR_inverseT r (ARapartT_wd r r (inject_Q_AR 0) (' zero0) (reflexivity r) AR_zero rnz)). rewrite H5. symmetry. apply AR_one. 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