proposition: Lemma CRmult_le_compat_l_half : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), 0 < r -> r1 <= r2 -> r * r1 <= r * r2.
proof: Proof. intros. intro abs. apply CRmult_lt_reg_l in abs. - contradiction. - exact H. Qed.
imports: QArith Qabs Qround