proposition: Theorem prod_nm_prod_nm_f : forall (i j k l : nat) (f : nat -> nat -> nat), prod_nm i j (fun x => prod_nm k (S l) (fun y => f x y)) = prod_nm i j (fun x => prod_nm k l (fun y => f x y) * f x (k + S l)).
proof: Proof. intros; apply prod_nm_ext; intros; rewrite prod_nm_f; auto. Qed.
imports: Coq(Arith ArithRing) Bertrand(Power)