# HG changeset patch
# User paulson
# Date 957797898 -7200
# Node ID d6122f13b8a6f8f3bd0de35aecc6c9cd3a73dd22
# Parent  bcceda950cd01a6fb385d71dc6f8e6515ce25abe
moved le_square, proved le_cube

diff -r bcceda950cd0 -r d6122f13b8a6 src/HOL/Arith.ML
--- 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";