(* Exercise coq_nat_02 *)

(* In the previous exercise we defined natural numbers and a plus
   operation on them. As a matter of fact those definitions (and
   many more) are part of the standard library of Coq, see:
     http://coq.inria.fr/library-eng.html
   They are part of the core library which is loaded automatically
   when Coq is started.
*)
Print nat.
Print plus.

(* Moreover Coq introduces notations for natural numbers allowing
   to write '0' for zero (instead of the letter 'O'), '+' for
   'plus' (with the infix notation) and to use decimal numbers
   instead of the unary notation with 'S'. *)
Check (2 + 2).

(* In the previous exercise we proved that '0 + n = n' and a very
   simple proof it was. Now let us try to prove 'n + 0 = n'. This
   is slightly more difficult. Can you see why? How would you prove
   that? *)

Lemma plus_zero_r : forall n, n + 0 = n.

Proof.
intros.
induction n.
(* You can also do
     elim n
   which is is the "primitive" tactic, but then you have to do additional
   intros
  You can also do 
     destruct n
  but that doesn't give you an induction hypothesis, only case distinction
*)
simpl.
reflexivity.
simpl.
rewrite -> IHn.
reflexivity.

Qed.