proposition: Theorem sum_bounded_permutation n i j g f : bounded_permut n i j g -> ∑ n f = ∑ n (fun i => f (g i)).
proof: Proof. intros [ H1 H2 H3 H4 H5 ]. destruct (lt_eq_lt_dec i j) as [ [ G1 | G1 ] | G1 ]. + apply sum_permutation_1 with i j; auto; split; auto. + apply msum_ext; rewrite <- G1 in *; clear j G1. intros j Hj; f_equal. destruct (eq_nat_dec j i); subst; auto. rewrite H5; auto. + apply sum_permutation_1 with j i; auto; split; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)