proposition: Lemma Rrepr_inv : forall (x:R) (xnz : Rrepr x # 0), Rrepr (/ x) == (/ Rrepr x) xnz.
proof: Proof. intros. rewrite RinvImpl.Rinv_def. destruct (Req_appart_dec x R0). - exfalso. subst x. destruct xnz. + rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c). + rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c). - rewrite Rquot2. apply (CReal_mult_eq_reg_l (Rrepr x)). + exact xnz. + rewrite CReal_mult_comm, (CReal_mult_comm (Rrepr x)), CReal_inv_l, CReal_inv_l. reflexivity. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions