proposition: Lemma CReal_mult_le_compat_l_half : forall r r1 r2, 0 < r -> r1 <= r2 -> r * r1 <= r * r2.
proof: Proof. intros. intro abs. apply (CReal_mult_lt_reg_l) in abs. - contradiction. - apply H. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra