proposition: Lemma Rmult_minus_distr_r : forall r1 r2 r3, (r2 - r3) * r1 = r2 * r1 - r3 * r1.
proof: Proof. intros r1 r2 r3; rewrite 3(Rmult_comm _ r1). now apply Rmult_minus_distr_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField