--- a/src/HOL/Arith.ML Mon May 08 16:57:53 2000 +0200
+++ b/src/HOL/Arith.ML Mon May 08 16:58:18 2000 +0200
@@ -337,12 +337,6 @@
Addsimps [mult_is_0, zero_is_mult];
-Goal "m <= m*(m::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
-by (etac (le_add2 RSN (2,le_trans)) 1);
-qed "le_square";
-
(*** Difference ***)
@@ -1044,6 +1038,17 @@
(* End of proof procedures. Now go and USE them! *)
(*---------------------------------------------------------------------------*)
+Goal "m <= m*(m::nat)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "le_square";
+
+Goal "(m::nat) <= m*(m*m)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "le_cube";
+
+
(*** Subtraction laws -- mostly from Clemens Ballarin ***)
Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";