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