title: How to prove mathematical induction formulae in LEAN theorem prover?
body: <p>Can anyone help me understand how to write the proof of a simple result that can be easily obtained by induction, for example the formula for the sum of the first <code>n</code> natural numbers: <code>1+2+...+n = n(n+1)/2</code>, using the LEAN theorem prover?</p>