{A : AbGroup} (m n : nat) (f : forall i j, (i < m)%nat -> (j < n)%nat -> A) : ab_sum m (fun i Hi => ab_sum n (fun j Hj => f i j Hi Hj)) = ab_sum n (fun j Hj => ab_sum m (fun i Hi => f i j Hi Hj)). Proof. induction n as [|n IHn] in m, f |- *. 1: by nrapply ab_sum_zero. lhs nrapply ab_sum_plus; cbn; f_ap. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Spaces.Nat.Core Spaces.Int. Require Import AbelianGroup.