proposition: Fact sum_0n_distr_l b n f : ∑ n (fun i => b⊗f i) = b⊗∑ n f.
proof: Proof. Proof using M_sum M_times sum_cancel distr_l. revert f; induction n as [ | n IHn ]; intros f. + do 2 rewrite msum_0; rewrite times_zero_r; auto. + do 2 rewrite msum_S; rewrite IHn, distr_l; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)