proposition: Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 = r1 * r2.
proof: Proof. intros r1 r2. now rewrite <-Ropp_mult_distr_l, <-Ropp_mult_distr_r, Ropp_involutive. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField