We show that 1+ 2+ ... + n equals n(n+1) / 2 .
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 {0,s} for NAT.

Induction requires that we do the following:

  1. base case: prove the assertion for n = 0.
  2. induction step: prove the assertion for s n assuming it for n.
We assume associativity and commutativity of the operation + by giving it assoc and comm attributes. (Proofs of these lemmas will be available soon.)
26 October 1996