fact: Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal := match xnz with | inl xNeg => - CReal_inv_pos (-x) (CReal_neg_lt_pos x xNeg) | inr xPos => CReal_inv_pos x xPos end.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra