Inductive nattree : Set :=
| leaf : nattree
| node : nattree -> nat -> nattree -> nattree.

Print nattree_ind.

Inductive mynat : Set :=
| zero : mynat
| succ : mynat -> mynat.

Print nat.
Print plus.
Eval compute in (plus 3 5).

Fixpoint add (n m : nat) { struct m } : nat :=
match m with 
| O => n
| S m' => S (add n m')
end.

Theorem OnotS : forall n, O <> S n.
intros n H.
inversion H.
Qed.

Theorem injS  : forall n m, S n = S m -> n = m.
intros n m H.
inversion H.
reflexivity.
Qed.

Theorem respS : forall n m, n = m -> S n = S m.
intros n m H.
rewrite H.
reflexivity.
Qed.

Theorem injS' : forall n m, n <> m -> S n <> S m.
intros n m N P.
apply N.
apply injS.
assumption.
Qed.

Theorem nNotSn : forall n, n <> S n.
induction n.
 apply OnotS.
apply injS'.
assumption.
Qed.

Theorem addNO : forall n, add n 0 = n.
simpl.
reflexivity.
Qed.

Theorem addON : forall n, add 0 n = n.
induction n.
 reflexivity.
simpl.
apply respS.
assumption.
Qed.

Print addON.

Implicit Arguments respS [ n m ].

Definition addON' : forall n, add O n = n :=
nat_ind (fun n => add O n = n)
        (refl_equal O)
        (fun n IHn => respS IHn).