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