proposition: Lemma Ropp_mult_distr_l : forall r1 r2, - (r1 * r2) = - r1 * r2.
proof: Proof. intros r1 r2; symmetry; apply Rplus_opp_r_uniq. now rewrite <-Rmult_plus_distr_r, Rplus_opp_r, Rmult_0_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField