proposition: Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
proof: Proof. intros. rewrite RinvImpl.Rinv_def; destruct (Req_appart_dec r R0). - contradiction. - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply CReal_inv_l. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions