proposition: Theorem sum_nm_com : forall (i j k l : nat) (f : nat -> nat -> nat), sum_nm i j (fun x => sum_nm k l (fun y => f x y)) = sum_nm k l (fun y => sum_nm i j (fun x => f x y)).
proof: Proof. intros i j; elim j. simpl in |- *; auto. intros j1 Rec; intros k l; case l. simpl in |- *; auto. intros l1 f; repeat rewrite sum_nm_f || rewrite sum_nm_sum_nm_f. rewrite <- sum_nm_add with (f := fun x => sum_nm k l1 (fun y : nat => f x y)) (g := fun x => f x (k + S l1)). rewrite (Rec k l1). rewrite <- sum_nm_add with (f := fun x => sum_nm i j1 (fun y : nat => f y x)) (g := fun x => f (i + S j1) x). replace (sum_nm k l1 (fun y : nat => sum_nm i j1 (fun x : nat => f x y)) + sum_nm i j1 (fun x : nat => f x (k + S l1)) + (sum_nm k l1 (fun y : nat => f (i + S j1) y) + f (i + S j1) (k + S l1))) with (sum_nm k l1 (fun y : nat => sum_nm i j1 (fun x : nat => f x y)) + sum_nm k l1 (fun y : nat => f (i + S j1) y) + (sum_nm i j1 (fun x : nat => f x (k + S l1)) + f (i + S j1) (k + S l1))). auto. ring; auto. Qed.
imports: Coq(Arith ArithRing)