proposition: Theorem sum_composed_permutation n f g : composed_permutation n g -> ∑ n f = ∑ n (fun i => f (g i)).
proof: Proof. induction 1 as [ g Hg | g i j p q H1 H2 IH2 H3 ]. + symmetry; apply msum_ext; intros; f_equal; apply Hg; auto. + rewrite IH2, sum_bounded_permutation with (1 := H1). symmetry; apply msum_ext; intros; f_equal; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)