added Suc_le_D

--- a/src/HOL/Nat.ML	Fri Feb 18 20:24:40 2000 +0100
+++ b/src/HOL/Nat.ML	Fri Feb 18 20:24:56 2000 +0100
@@ -57,6 +57,11 @@
 qed "not_gr0";
 AddIffs [not_gr0];
 
+Goal "(Suc n <= m') --> (? m. m' = Suc m)";
+by (induct_tac "m'" 1);
+by  Auto_tac;
+qed_spec_mp "Suc_le_D";
+
 (*Useful in certain inductive arguments*)
 Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
 by (exhaust_tac "m" 1);