We use induction on

`NAT`

to prove
(N : Nat) sum(N)+ sum(N) = N * s N.

For this, we use the induction scheme based on the signature

`NAT`

.
Induction requires that we do the following:

**base case:**prove the assertion for*n = 0*.**induction step:**prove the assertion for*s n*assuming it for*n*.

`assoc`

and `comm`

attributes. (Proofs of these lemmas
will be available soon.)
26 October 1996