proposition: Theorem sum_nm_sum_nm_f : forall (i j k l : nat) (f : nat -> nat -> nat), sum_nm i j (fun x => sum_nm k (S l) (fun y => f x y)) = sum_nm i j (fun x => sum_nm k l (fun y => f x y) + f x (k + S l)).
proof: Proof. intros; apply sum_nm_ext; intros; rewrite sum_nm_f; auto. Qed.
imports: Coq(Arith ArithRing)