# HG changeset patch
# User haftmann
# Date 1237751171 -3600
# Node ID fbd548c4bb6a76886be5ff59f31a5f081ac65c77
# Parent  752329615264251bf56c3d1526955d426c4c2d9e
lemma nat_dvd_not_less moved here from Arith_Tools

diff -r 752329615264 -r fbd548c4bb6a 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