proposition: Fact sum_0n_scal_r n k f : ∑ n (fun i => (f i)*k) = (∑ n f)*k.
proof: Proof. apply sum_0n_distr_r with (3 := Nat_mult_monoid); auto. intros; ring. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)