src/HOL/Divides.thy
 changeset 63499 9c9a59949887 parent 63417 c184ec919c70 child 63834 6a757f36997e
```     1.1 --- a/src/HOL/Divides.thy	Wed Jul 13 15:46:52 2016 +0200
1.2 +++ b/src/HOL/Divides.thy	Thu Jul 14 14:43:09 2016 +0200
1.3 @@ -128,12 +128,12 @@
1.4    "a mod a = 0"
1.5    using mod_mult_self2_is_0 [of 1] by simp
1.6
1.9    assumes "b \<noteq> 0"
1.10    shows "(b + a) div b = a div b + 1"
1.11    using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
1.12
1.15    assumes "b \<noteq> 0"
1.16    shows "(a + b) div b = a div b + 1"
1.18 @@ -1116,7 +1116,7 @@
1.19  proof -
1.20    from \<open>m \<ge> n\<close> obtain q where "m = n + q"
1.22 -  with \<open>n > 0\<close> show ?thesis by simp
1.23 +  with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
1.24  qed
1.25
1.26  lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
1.27 @@ -2154,7 +2154,7 @@
1.28  proof -
1.29    have "k = (k - l) + l" by simp
1.30    then obtain j where k: "k = j + l" ..
1.31 -  with assms show ?thesis by simp