src/HOL/Divides.thy
changeset 63317 ca187a9f66da
parent 63145 703edebd1d92
child 63417 c184ec919c70
     1.1 --- a/src/HOL/Divides.thy	Wed Jun 15 15:52:24 2016 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Jun 16 17:57:09 2016 +0200
     1.3 @@ -363,6 +363,23 @@
     1.4  lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
     1.5  by (blast intro: dvd_mod_imp_dvd dvd_mod)
     1.6  
     1.7 +lemma div_div_eq_right:
     1.8 +  assumes "c dvd b" "b dvd a"
     1.9 +  shows   "a div (b div c) = a div b * c"
    1.10 +proof -
    1.11 +  from assms have "a div b * c = (a * c) div b"
    1.12 +    by (subst dvd_div_mult) simp_all
    1.13 +  also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp
    1.14 +  also have "a * c div (b div c * c) = a div (b div c)"
    1.15 +    by (cases "c = 0") simp_all
    1.16 +  finally show ?thesis ..
    1.17 +qed
    1.18 +
    1.19 +lemma div_div_div_same:
    1.20 +  assumes "d dvd a" "d dvd b" "b dvd a"
    1.21 +  shows   "(a div d) div (b div d) = a div b"
    1.22 +  using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
    1.23 +
    1.24  end
    1.25  
    1.26  class ring_div = comm_ring_1 + semiring_div