proposition: Lemma sum_mull f (k n : nat) : k * (\sum_(0 <= i < n) f i) = \sum_(0 <= i < n) (k * f i).
proof: Proof. by apply: (big_morph (fun n => k * n)) => [x y|]; [rewrite mulnDr | rewrite muln0]. Qed.
imports: mathcomp(all_ssreflect)