proposition: Lemma CRmult_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), 0 < r -> r1 < r2 -> r1 * r < r2 * r.
proof: Proof. intros. apply (CRplus_lt_reg_r (CRopp R (CRmult R r1 r))). apply (CRle_lt_trans _ 0). 1:apply (Ropp_def (CRisRing R)). apply (CRlt_le_trans _ (CRplus R (CRmult R r2 r) (CRmult R (CRopp R r1) r))). 1:apply (CRlt_le_trans _ (CRmult R (CRplus R r2 (CRopp R r1)) r)). - apply CRmult_lt_0_compat. 2: exact H. apply (CRplus_lt_reg_r r1). apply (CRle_lt_trans _ r1). + apply (Radd_0_l (CRisRing R)). + apply (CRlt_le_trans _ r2 _ H0). apply (CRle_trans _ (CRplus R r2 (CRplus R (CRopp R r1) r1))). 1:apply (CRle_trans _ (CRplus R r2 0)). * destruct (CRplus_0_r r2). exact H1. * apply CRplus_le_compat_l. destruct (CRplus_opp_l r1). exact H1. * destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2. - destruct (CRisRing R). destruct (Rdistr_l r2 (CRopp R r1) r). exact H2. - apply CRplus_le_compat_l. destruct (CRopp_mult_distr_l r1 r). exact H1. Qed.
imports: QArith Qabs Qround