proposition: Theorem prod_nm_com : forall (i j k l : nat) (f : nat -> nat -> nat), prod_nm i j (fun x => prod_nm k l (fun y => f x y)) = prod_nm k l (fun y => prod_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 prod_nm_f || rewrite prod_nm_prod_nm_f. rewrite <- prod_nm_mult with (f := fun x => prod_nm k l1 (fun y : nat => f x y)) (g := fun x => f x (k + S l1)). rewrite (Rec k l1). rewrite <- prod_nm_mult with (f := fun x => prod_nm i j1 (fun y : nat => f y x)) (g := fun x => f (i + S j1) x). replace (prod_nm k l1 (fun y : nat => prod_nm i j1 (fun x : nat => f x y)) * prod_nm i j1 (fun x : nat => f x (k + S l1)) * (prod_nm k l1 (fun y : nat => f (i + S j1) y) * f (i + S j1) (k + S l1))) with (prod_nm k l1 (fun y : nat => prod_nm i j1 (fun x : nat => f x y)) * prod_nm k l1 (fun y : nat => f (i + S j1) y) * (prod_nm i j1 (fun x : nat => f x (k + S l1)) * f (i + S j1) (k + S l1))). Proof. auto. ring; auto. Qed.
imports: Coq(Arith ArithRing) Bertrand(Power)