proposition: Fact msum_fold_map n f : ∑ n f = fold_right m u (map f (list_an 0 n)).
proof: Proof. revert f; induction n as [ | n IHn ]; intros f; simpl; f_equal; auto. rewrite IHn, <- map_S_list_an, map_map; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)