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