src/HOL/Divides.thy
changeset 65556 fcd599570afa
parent 64848 c50db2128048
child 66630 034cabc4fda5
--- a/src/HOL/Divides.thy	Sun Apr 23 14:53:33 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Apr 23 14:53:35 2017 +0200
@@ -164,6 +164,15 @@
 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   unfolding dvd_def by (auto simp add: mod_mult_mult1)
 
+lemma div_plus_div_distrib_dvd_left:
+  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
+  by (cases "c = 0") (auto elim: dvdE)
+
+lemma div_plus_div_distrib_dvd_right:
+  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
+  using div_plus_div_distrib_dvd_left [of c b a]
+  by (simp add: ac_simps)
+
 named_theorems mod_simps
 
 text \<open>Addition respects modular equivalence.\<close>