more lemmas
authorhaftmann
Sun Apr 23 14:53:35 2017 +0200 (2017-04-23)
changeset 65556fcd599570afa
parent 65555 85ed070017b7
child 65568 1070be576372
more lemmas
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Apr 23 14:53:33 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Apr 23 14:53:35 2017 +0200
     1.3 @@ -164,6 +164,15 @@
     1.4  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
     1.5    unfolding dvd_def by (auto simp add: mod_mult_mult1)
     1.6  
     1.7 +lemma div_plus_div_distrib_dvd_left:
     1.8 +  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
     1.9 +  by (cases "c = 0") (auto elim: dvdE)
    1.10 +
    1.11 +lemma div_plus_div_distrib_dvd_right:
    1.12 +  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
    1.13 +  using div_plus_div_distrib_dvd_left [of c b a]
    1.14 +  by (simp add: ac_simps)
    1.15 +
    1.16  named_theorems mod_simps
    1.17  
    1.18  text \<open>Addition respects modular equivalence.\<close>