src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Sun Mar 22 20:46:10 2009 +0100
+++ b/src/HOL/Divides.thy	Sun Mar 22 20:46:11 2009 +0100
@@ -1148,4 +1148,9 @@
   with j show ?thesis by blast
 qed
 
+lemma nat_dvd_not_less:
+  fixes m n :: nat
+  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
 end