arith.ML

 by (rtac le_add2 1);
 val le_add1 = result();
 
 val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
 val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
+
+goal Arith.thy "m+k<=n --> m<=n::nat";
+by(nat_ind_tac "k" 1);
+by(ALLGOALS(simp_tac arith_ss));
+by(fast_tac (HOL_cs addDs [Suc_leD]) 1);
+val plus_leD1 = result() RS mp;