proposition: Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) = r1 * - r2.
proof: Proof. now intros r1 r2; rewrite 2(Rmult_comm r1); apply Ropp_mult_distr_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField