(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/orders.ma".
+set "baseuri" "cic:/matita/nat/orders".
include "logic/connectives.ma".
include "logic/equality.ma".
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 x).assumption.
+elim H.apply le_n.apply trans_le ? (pred e2).assumption.
apply le_pred_n.
qed.