Induction step for (N : Nat) sum(N)+ sum(N) = N * s N .
We use quantifier elimination, implication elimination, lemma introduction, and reduction to show that
( N : Nat) (sum(N) + sum(N) = N * (s N)   implies
                  sum(s N) + sum(s N) = (s N) * (s s N)) .
This involves the following steps:
  1. introduce a new constant n of sort Nat.
  2. assume sum(n)+ sum(n) = n * (s n) .
  3. introduce the lemma ( M, N : Nat) (s M) * N = (M * N) + N .
  4. show sum(s n)+ sum(s n) = (s n) * (s s n) by reduction.

26 October 1996