+theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+intro.elim n.apply False_ind.exact not_le_Sn_O O H.
+apply eq_f.apply pred_Sn.
+qed.
+
+theorem nat_compare_pred_pred:
+\forall n,m:nat.lt O n \to lt O m \to
+eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
+intros.
+apply lt_O_n_elim n H.
+apply lt_O_n_elim m H1.
+intros.
+simplify.reflexivity.
+qed.
+