proposition: Lemma CRmult_le_compat_r : forall {R : ConstructiveReals} (r r1 r2:CRcarrier R), 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
proof: Proof. intros. do 2 rewrite <- (CRmult_comm r). apply CRmult_le_compat_l; assumption. Qed.
imports: QArith Qabs Qround