theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m.
intros.change with le (pred (S n)) (pred (S m)).
-elim H.apply le_n.apply trans_le ? (pred e2).assumption.
+elim H.apply le_n.apply trans_le ? (pred n1).assumption.
apply le_pred_n.
qed.
qed.
theorem not_le_Sn_n: \forall n:nat. Not (le (S n) n).
-intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S e1) e1.
+intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S n1) n1.
apply H.assumption.
apply le_S_S_to_le.assumption.
qed.