qed.
theorem injective_S : injective nat nat S.
-simplify.
+unfold injective.
intros.
rewrite > pred_Sn.
rewrite > (pred_Sn y).
theorem not_eq_S : \forall n,m:nat.
\lnot n=m \to S n \neq S m.
-intros. simplify. intros.
+intros. unfold Not. intros.
apply H. apply injective_S. assumption.
qed.
| (S p) \Rightarrow True ].
theorem not_eq_O_S : \forall n:nat. O \neq S n.
-intros. simplify. intros.
+intros. unfold Not. intros.
cut (not_zero O).
exact Hcut.
rewrite > H.exact I.
qed.
theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
-intros.simplify.
+intros.unfold decidable.
apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
intro.elim n1.
left.reflexivity.