automatic classical rule to derive a dvd b from b mod a = 0
authorhaftmann
Tue May 22 18:14:29 2018 +0000 (21 months ago)
changeset 682528b284d24f434
parent 68251 54a127873735
child 68253 a8660a39e304
automatic classical rule to derive a dvd b from b mod a = 0
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Rings.thy	Tue May 22 18:14:29 2018 +0000
     1.2 +++ b/src/HOL/Rings.thy	Tue May 22 18:14:29 2018 +0000
     1.3 @@ -1712,7 +1712,7 @@
     1.4    "b mod a = 0" if "a dvd b"
     1.5    using that minus_div_mult_eq_mod [of b a] by simp
     1.6  
     1.7 -lemma mod_0_imp_dvd: 
     1.8 +lemma mod_0_imp_dvd [dest!]: 
     1.9    "b dvd a" if "a mod b = 0"
    1.10  proof -
    1.11    have "b dvd (a div b) * b" by simp