fact: Definition CReal_mult_lt_0_compat : forall x y : CReal, 0 < x -> 0 < y -> 0 < x * y := fun x y Hx Hy => exist _ (proj1_sig Hx + proj1_sig Hy - 1)%Z (CReal_mult_lt_0_compat_correct x y Hx Hy).
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra