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 []