proposition: Lemma CRmult_inv_r : forall (x : CR) (xnz : (x >< 0)%CR), x * CRinvT x xnz == 1.
proof: Proof. intros. destruct xnz as [neg|pos]. - pose proof neg as otherNeg. destruct neg as [q neg]. unfold CRinvT. setoid_replace (x * - CRinv_pos q (- x))%CR with (-x * CRinv_pos q (- x))%CR by (unfold equiv, msp_Equiv; ring). apply CRopp_lt_compat in otherNeg. apply (CRltT_wd CRopp_0 (reflexivity _)) in otherNeg. pose proof (CRmult_inv_r_pos (-x)%CR (inr otherNeg) otherNeg). pose proof (CRinvT_pos_inv q (inr otherNeg)). destruct otherNeg as [r H1]. unfold CRinvT in H. unfold CRinvT in H0. rewrite H0. exact H. rewrite CRplus_0_l in neg. exact neg. - apply CRmult_inv_r_pos, pos. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders