proposition: Lemma CReal_inv_1 : forall nz : 1 # 0, (/ 1) nz == 1.
proof: Proof. intros. rewrite <- (CReal_mult_1_l ((/1) nz)). rewrite CReal_inv_r. reflexivity. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra