proposition: Lemma CRmult_eq_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), 0 ≶ r -> r1 * r == r2 * r -> r1 == r2.
proof: Proof. intros. destruct H0,H. - split. + intro abs. apply H0. apply CRmult_lt_compat_r. * exact c. * exact abs. + intro abs. apply H1. apply CRmult_lt_compat_r. * exact c. * exact abs. - split. + intro abs. apply H1. apply CRopp_lt_cancel. apply (CRle_lt_trans _ (CRmult R r1 (CRopp R r))). { apply CRopp_mult_distr_r. } apply (CRlt_le_trans _ (CRmult R r2 (CRopp R r))). 2: apply CRopp_mult_distr_r. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). { apply (Radd_0_l (CRisRing R)). } apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. + intro abs. apply H0. apply CRopp_lt_cancel. apply (CRle_lt_trans _ (CRmult R r2 (CRopp R r))). 1:apply CRopp_mult_distr_r. apply (CRlt_le_trans _ (CRmult R r1 (CRopp R r))). 2: apply CRopp_mult_distr_r. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). 1:apply (Radd_0_l (CRisRing R)). apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. Qed.
imports: QArith Qabs Qround