[mizar] Has someone done that?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

Peter Koepke from Bonn (koepke@math.uni-bonn.de) wrote me this

	I was in vain looking for a Mizar proof of
	the summation formula

	$1+2+3+\dots+n = \frac{1}{2}n^2 + \frac{1}{2}n$

I vaguely recall that someone (Andrzej?) has proven this some time ago.
I cannot find it.  AFAIK, Peter would like to have an expository proof
of it.  I could do it but maybe someone has got it already?


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr