# HG changeset patch
# User haftmann
# Date 1383216260 -3600
# Node ID 24874b4024d1722f4992e115dff94f8cdb2e3ed3
# Parent  56587960e444f5bd5585cb19f35c548830d3db04
generalised lemma

diff -r 56587960e444 -r 24874b4024d1 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -1872,12 +1872,12 @@
   shows "m dvd n + q \<longleftrightarrow> m dvd n"
   using assms by (simp add: dvd_plus_eq_right add_commute [of n])
 
-lemma less_dvd_minus:
+lemma less_eq_dvd_minus:
   fixes m n :: nat
-  assumes "m < n"
-  shows "m dvd n \<longleftrightarrow> m dvd (n - m)"
+  assumes "m \<le> n"
+  shows "m dvd n \<longleftrightarrow> m dvd n - m"
 proof -
-  from assms have "n = m + (n - m)" by arith
+  from assms have "n = m + (n - m)" by simp
   then obtain q where "n = m + q" ..
   then show ?thesis by (simp add: dvd_reduce add_commute [of m])
 qed
diff -r 56587960e444 -r 24874b4024d1 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -75,7 +75,7 @@
 lemma numbers_of_marks_mark_out:
   "numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
   by (auto simp add: numbers_of_marks_def mark_out_def in_set_enumerate_eq image_iff
-    nth_enumerate_eq less_dvd_minus)
+    nth_enumerate_eq less_eq_dvd_minus)
 
 
 text {* Auxiliary operation for efficient implementation  *}
@@ -128,7 +128,7 @@
     by (simp add: mark_out_aux_def)
   show ?thesis2
     by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def
-      enumerate_Suc_eq in_set_enumerate_eq less_dvd_minus)
+      enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus)
   { def v \<equiv> "Suc m" and w \<equiv> "Suc n"
     fix q
     assume "m + n \<le> q"