proposition: Lemma CRmult_inv_r_nlt : (forall (r : CR) (rnz : (fun x y : CR => ((x < y)%CR + (y < x)%CR)%type) r 0%CR), (fun x y : CR => (fun x0 y0 : CR => (y0 < x0)%CR -> False) y x /\ (fun x0 y0 : CR => (y0 < x0)%CR -> False) x y) (CRinvT r rnz * r)%CR 1%CR).
proof: Proof. intros. apply CReq_nlt. rewrite CRmult_comm. apply CRmult_inv_r. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon