proposition: Lemma Rmult_minus_distr_l : forall r1 r2 r3, r1 * (r2 - r3) = r1 * r2 - r1 * r3.
proof: Proof. unfold Rminus; intros r1 r2 r3; rewrite Rmult_plus_distr_l. now rewrite Ropp_mult_distr_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField