proposition: Lemma Rmult_minus_distr_r: forall r1 r2 r3 : R, (r1 - r2) * r3 = r1 * r3 - r2 * r3.
proof: Proof. intros. unfold Rminus. rewrite <- Ropp_mult_distr_l_reverse. apply Rmult_plus_distr_r. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)