proposition: Lemma sum_nm_add : forall (n m : nat) (f g : nat -> nat), sum_nm n m f + sum_nm n m g = sum_nm n m (fun i : nat => f i + g i).
proof: Proof. intros n m f g; generalize n; clear n; elim m; simpl in |- *; auto. intros m' Rec n. rewrite <- Rec. ring. Qed.
imports: Coq(Arith ArithRing)