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