proposition: Theorem sum_injective n f g : bounded_injective n g -> ∑ n f = ∑ n (fun i => f (g i)).
proof: Proof. intros; apply sum_composed_permutation, injective_composed_permutation; trivial. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)