% Starting the specification of natural numbers
% Definition and theorems regarding the just the nat predicate
Kind nat type.
Type z nat.
Type s nat -> nat.
Define nat : nat -> prop by nat z ; nat (s N) := nat N.
Define noteq : nat -> nat -> prop by
noteq z (s N) := nat N
; noteq (s N) z := nat N
; noteq (s M) (s N) := noteq M N.
Theorem noteq_types : forall N M, noteq N M -> (nat N /\ nat M).
induction on 1. intros. case H1. search. search. apply IH to H2. search.
Theorem nat_decide_zero: forall N, nat N -> N = z \/ exists M, nat M /\ N = (s M).
induction on 1. intros. case H1. left. search. right. search.
Theorem noteq_sym : forall N M, noteq N M -> noteq M N.
induction on 1. intros. case H1. search. search. apply IH to H2. search.
Theorem noteq_basic : forall N, nat N -> noteq (s N) N.
induction on 1. intros. case H1. search. apply IH to H2. search.
Theorem noteq_eq1 : forall N M, noteq N M -> N = M -> false.
induction on 1. intros. case H1. case H2. case H2. case H2. apply IH to H3 _.
Theorem noteq_eq2 : forall N M, nat N -> nat M -> (N = M -> false) -> noteq N M.
induction on 1. induction on 2. intros. case H1. case H2. apply H3 to _.
unfold. search. case H2. search. apply IH1 to H4 H5 _. intros. backchain H3. case H6. search. search.
Theorem nat_separate : forall N M, nat N -> nat M -> (N = M \/ noteq N M).
induction on 1. induction on 2. intros. case H1. case H2. left. search. right. unfold. search.
case H2. right. unfold. search. apply IH to H3 H4. case H5. left. search. right. unfold. search.
