project: Nat

*** ***********************************************************

proof: <<SumThm>> 
  spec: /home/klin/obj3/nat.obj
  goal: (forall N : Nat) sum(N) + sum(N) = N * s N  .

by: induction on N by scheme {0, s} []

*** ************************************************************

display:
  title: "Sum of the First n Natural Numbers"
  putdir: /net/cs/htdocs/groups/tatami/demos/nat/sum
  gethomepage: /home/klin/tmp/sum/home.html
  getspecexpl: /home/klin/tmp/sum/specexp.html

<<SumThm>>
  subtitle: "We show that <math>1+...+n</math> equals <math>n(n+1)/2</math>. "
  getexpl:  /home/klin/tmp/sum/exp.html
[]