proposition: Lemma CReal_inv_r : forall (r:CReal) (rnz : r # 0), r * ((/ r) rnz) == 1.
proof: Proof. intros. rewrite CReal_mult_comm, CReal_inv_l. reflexivity. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra