+theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
+intros.simplify.
+apply nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))).
+intro.elim n1.
+left.reflexivity.
+right.apply not_eq_O_S.
+intro.right.intro.
+apply not_eq_O_S n1.
+apply sym_eq.assumption.
+intros.elim H.
+left.apply eq_f. assumption.
+right.intro.apply H1.apply inj_S.assumption.
+qed.
+