Example of proof by elimination with Coq from Coq Art

ex6_29.v

(* exercise 6.29 from Coq Art *)

Check eq_ind.

(*
 eq_ind
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, x = y -> P y 
*)

Theorem plus_n_O : forall n, n + 0 = n.
Proof.
  intro n; elim n.
  reflexivity.
  simpl; intros n0 H.
  apply eq_ind
    with (x := n0 + 0) (P := fun y => S(n0 + 0) = S y).
  reflexivity.
  assumption.
Qed.

Problem:

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