src/HOL/Rings.thy
changeset 66808 1907167b6038
parent 66807 c3631f32dfeb
child 66810 cc2b490f9dc4
     1.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -1620,6 +1620,10 @@
     1.4    shows "c dvd a"
     1.5    using assms dvd_mod_iff [of c b a] by simp
     1.6  
     1.7 +lemma dvd_minus_mod [simp]:
     1.8 +  "b dvd a - a mod b"
     1.9 +  by (simp add: minus_mod_eq_div_mult)
    1.10 +
    1.11  end
    1.12  
    1.13  class idom_modulo = idom + semidom_modulo