A simple proof by elimination

Prove the following theorem, using only the following tactics : intros, assumption, elim, simpl, and reflexivity.
Theorem plus_n_O : forall n, n+0 =n.

Solution

Look at this file