# HG changeset patch
# User haftmann
# Date 1492952015 -7200
# Node ID fcd599570afa4ad1b24b7e137d34846b93a8232c
# Parent  85ed070017b7465118aecf638a20314c37450fe3
more lemmas

diff -r 85ed070017b7 -r fcd599570afa src/HOL/Divides.thy
--- 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>