src/HOL/Nat.thy
changeset 54222 24874b4024d1
parent 54147 97a8ff4e4ac9
child 54223 85705ba18add
     1.1 --- a/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -1872,12 +1872,12 @@
     1.4    shows "m dvd n + q \<longleftrightarrow> m dvd n"
     1.5    using assms by (simp add: dvd_plus_eq_right add_commute [of n])
     1.6  
     1.7 -lemma less_dvd_minus:
     1.8 +lemma less_eq_dvd_minus:
     1.9    fixes m n :: nat
    1.10 -  assumes "m < n"
    1.11 -  shows "m dvd n \<longleftrightarrow> m dvd (n - m)"
    1.12 +  assumes "m \<le> n"
    1.13 +  shows "m dvd n \<longleftrightarrow> m dvd n - m"
    1.14  proof -
    1.15 -  from assms have "n = m + (n - m)" by arith
    1.16 +  from assms have "n = m + (n - m)" by simp
    1.17    then obtain q where "n = m + q" ..
    1.18    then show ?thesis by (simp add: dvd_reduce add_commute [of m])
    1.19  qed