nat.ML

 goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
 by(simp_tac (HOL_ss addsimps [less_Suc_eq]) 1);
 by (fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym]) 1);
 val lessD = result();
 
+goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
+by(asm_full_simp_tac (HOL_ss addsimps [less_Suc_eq]) 1);
+by(fast_tac HOL_cs 1);
+val Suc_leD = result();
+
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= n::nat";
 by (fast_tac (HOL_cs addEs [less_anti_sym]) 1);
 val less_imp_le = result();
 
 goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=n::nat";