proposition: Lemma CReal_mult_le_reg_l : forall x y z : CReal, 0 < x -> x * y <= x * z -> y <= z.
proof: Proof. intros. intro abs. apply (CReal_mult_lt_compat_l x) in abs. - contradiction. - exact H. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra