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