proposition: Theorem sum_bijection n f g h : bijection n g h -> ∑ n f = ∑ n (fun i => f (g i)).
proof: Proof. intros [ H1 H2 H3 H4 ]. apply sum_injective. constructor; auto. intros i j G1 G2 G3; rewrite <- (H4 i), G3; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)