tuned
authorhaftmann
Thu Nov 23 17:03:20 2017 +0000 (17 months ago)
changeset 67084e138d96ed083
parent 67083 6b2c0681ef28
child 67085 f5d7f37b4143
tuned
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Rings.thy	Thu Nov 23 13:00:00 2017 +0000
     1.2 +++ b/src/HOL/Rings.thy	Thu Nov 23 17:03:20 2017 +0000
     1.3 @@ -1699,17 +1699,15 @@
     1.4    using div_mult_mod_eq [of a a] by simp
     1.5  
     1.6  lemma dvd_imp_mod_0 [simp]:
     1.7 -  assumes "a dvd b"
     1.8 -  shows "b mod a = 0"
     1.9 -  using assms minus_div_mult_eq_mod [of b a] by simp
    1.10 +  "b mod a = 0" if "a dvd b"
    1.11 +  using that minus_div_mult_eq_mod [of b a] by simp
    1.12  
    1.13  lemma mod_0_imp_dvd: 
    1.14 -  assumes "a mod b = 0"
    1.15 -  shows   "b dvd a"
    1.16 +  "b dvd a" if "a mod b = 0"
    1.17  proof -
    1.18 -  have "b dvd ((a div b) * b)" by simp
    1.19 +  have "b dvd (a div b) * b" by simp
    1.20    also have "(a div b) * b = a"
    1.21 -    using div_mult_mod_eq [of a b] by (simp add: assms)
    1.22 +    using div_mult_mod_eq [of a b] by (simp add: that)
    1.23    finally show ?thesis .
    1.24  qed
    1.25