proposition: Lemma t_sum_Svars : forall (n m : nat) (f : nat -> nat), sum_nm n m f = sum_nm (S n) m (fun i : nat => f (pred i)).
proof: Proof. intros n m f; generalize n; clear n; elim m; simpl in |- *; auto. Qed.
imports: Coq(Arith ArithRing)