proposition: Lemma CRopp_mult_distr_l : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), - (r1 * r2) == (- r1) * r2.
proof: Proof. intros. transitivity (r2 * - r1). 1:transitivity (- (r2 * r1)). - apply (Ropp_ext (CRisRingExt R)). apply CReq_sym, (Rmul_comm (CRisRing R)). - apply CRopp_mult_distr_r. - apply CReq_sym, (Rmul_comm (CRisRing R)). Qed.
imports: QArith Qabs Qround