author | haftmann |
Sun, 22 Mar 2009 20:46:11 +0100 (2009-03-22) | |
changeset 30653 | fbd548c4bb6a |
parent 30652 | 752329615264 |
child 30654 | 254478a8dd05 |
--- 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