proposition: Fact msum_msum n k f : (forall i1 j1 i2 j2, i1 < n -> j1 < k -> i2 < n -> j2 < k -> f i1 j1 ⊕ f i2 j2 = f i2 j2 ⊕ f i1 j1) -> ∑ n (fun i => ∑ k (f i)) = ∑ k (fun j => ∑ n (fun i => f i j)).
proof: Proof. Proof using Hmonoid. revert k f; induction n as [ | n IHn ]; intros k f Hf. + rewrite msum_0, msum_of_unit; auto. + rewrite msum_S, IHn. * rewrite <- msum_sum. - apply msum_ext. intros; rewrite msum_S; trivial. - intros; symmetry; apply msum_comm. intros; apply Hf; lia. * intros; apply Hf; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)