proposition: Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), - (r1 * r2) == r1 * (- r2).
proof: Proof. intros. apply (CRplus_eq_reg_l (CRmult R r1 r2)). destruct (CRisRing R). transitivity (CR_of_Q R 0). 1:apply Ropp_def. transitivity (r1 * (r2 + - r2)). 2: apply CRmult_plus_distr_l. transitivity (r1 * 0). 1:apply CReq_sym, CRmult_0_r. destruct (CRisRingExt R). apply Rmul_ext. - apply CReq_refl. - apply CReq_sym, Ropp_def. Qed.
imports: QArith Qabs Qround