proposition: Lemma CRmult_le_compat_l : forall {R : ConstructiveReals} (r r1 r2:CRcarrier R), 0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
proof: Proof. intros. apply (CRplus_le_reg_r (-(r*r1))). rewrite CRplus_opp_r, CRopp_mult_distr_r. rewrite <- CRmult_plus_distr_l. apply CRmult_le_0_compat. - exact H. - apply (CRplus_le_reg_r r1). rewrite CRplus_0_l, CRplus_assoc, CRplus_opp_l, CRplus_0_r. exact H0. Qed.
imports: QArith Qabs Qround