proposition: Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0), ((/ r) rnz) * r == 1.
proof: Proof. intros. unfold CReal_inv. destruct rnz. - rewrite <- CReal_opp_mult_distr_l, CReal_opp_mult_distr_r. apply CReal_inv_l_pos. - apply CReal_inv_l_pos. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra