set "baseuri" "cic:/matita/nat/nat".
-include "logic/equality.ma".
-include "logic/connectives.ma".
-include "datatypes/bool.ma".
include "higher_order_defs/functions.ma".
inductive nat : Set \def
| (S p) \Rightarrow p ].
theorem pred_Sn : \forall n:nat.n=(pred (S n)).
-intros; reflexivity.
+intros. reflexivity.
qed.
theorem injective_S : injective nat nat S.
\def injective_S.
theorem not_eq_S : \forall n,m:nat.
-\lnot n=m \to \lnot (S n = S m).
+\lnot n=m \to S n \neq S m.
intros. simplify. intros.
apply H. apply injective_S. assumption.
qed.
[ O \Rightarrow False
| (S p) \Rightarrow True ].
-theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
+theorem not_eq_O_S : \forall n:nat. O \neq S n.
intros. simplify. intros.
cut (not_zero O).
exact Hcut.
rewrite > H.exact I.
qed.
-theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
+theorem not_eq_n_Sn : \forall n:nat. n \neq S n.
intros.elim n.
apply not_eq_O_S.
apply not_eq_S.assumption.
left.reflexivity.
right.apply not_eq_O_S.
intro.right.intro.
-apply not_eq_O_S n1 ?.
+apply not_eq_O_S n1.
apply sym_eq.assumption.
intros.elim H.
left.apply eq_f. assumption.