# HG changeset patch
# User paulson
# Date 1127898866 -7200
# Node ID 91d3604ec4b5143f97d1e4982d2176bb3daa7c27
# Parent  52157349e0065362f4d6a5ee83745c307399a09e
new lemma

diff -r 52157349e006 -r 91d3604ec4b5 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Wed Sep 28 09:14:44 2005 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Wed Sep 28 11:14:26 2005 +0200
@@ -640,19 +640,16 @@
 apply (auto simp add: poly_mult fun_eq real_mult_assoc)
 done
 
-lemma le_iff_add: "(m::nat) \<le> n = (\<exists>d. n = m + d)"
-by (auto simp add: le_eq_less_or_eq less_iff_Suc_add)
-
 lemma poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
 apply (auto simp add: le_iff_add)
-apply (induct_tac "d")
+apply (induct_tac k)
 apply (rule_tac [2] poly_divides_trans)
 apply (auto simp add: divides_def)
 apply (rule_tac x = p in exI)
 apply (auto simp add: poly_mult fun_eq mult_ac)
 done
 
-lemma poly_exp_divides: "[| (p %^ n) divides q;  m \<le> n |] ==> (p %^ m) divides q"
+lemma poly_exp_divides: "[| (p %^ n) divides q;  m\<le>n |] ==> (p %^ m) divides q"
 by (blast intro: poly_divides_exp poly_divides_trans)
 
 lemma poly_divides_add:
@@ -1119,7 +1116,6 @@
 val poly_primes = thm "poly_primes";
 val poly_divides_refl = thm "poly_divides_refl";
 val poly_divides_trans = thm "poly_divides_trans";
-val le_iff_add = thm "le_iff_add";
 val poly_divides_exp = thm "poly_divides_exp";
 val poly_exp_divides = thm "poly_exp_divides";
 val poly_divides_add = thm "poly_divides_add";
diff -r 52157349e006 -r 91d3604ec4b5 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Wed Sep 28 09:14:44 2005 +0200
+++ b/src/HOL/NatArith.thy	Wed Sep 28 11:14:26 2005 +0200
@@ -14,6 +14,9 @@
 
 text{*The following proofs may rely on the arithmetic proof procedures.*}
 
+lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
+  by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
+
 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
 by (simp add: less_eq reflcl_trancl [symmetric]
             del: reflcl_trancl, arith)