src/HOL/Divides.thy

 
 lemma div_mult_self2 [simp]:
   assumes "b \<noteq> 0"
   shows "(a + b * c) div b = c + a div b"
   using assms div_mult_self1 [of b a c] by (simp add: mult_commute)
+
+lemma div_mult_self3 [simp]:
+  assumes "b \<noteq> 0"
+  shows "(c * b + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
+
+lemma div_mult_self4 [simp]:
+  assumes "b \<noteq> 0"
+  shows "(b * c + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
 
 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
 proof (cases "b = 0")
   case True then show ?thesis by simp
 next

   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
     by (simp add: mod_div_equality)
   then show ?thesis by simp
 qed
 
-lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
+lemma mod_mult_self2 [simp]: 
+  "(a + b * c) mod b = a mod b"
   by (simp add: mult_commute [of b])
+
+lemma mod_mult_self3 [simp]:
+  "(c * b + a) mod b = a mod b"
+  by (simp add: add.commute)
+
+lemma mod_mult_self4 [simp]:
+  "(b * c + a) mod b = a mod b"
+  by (simp add: add.commute)
 
 lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
   using div_mult_self2 [of b 0 a] by simp
 
 lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"

 lemma div_minus1_right [simp]: "a div (-1) = -a"
   using div_minus_right [of a 1] by simp
 
 lemma mod_minus1_right [simp]: "a mod (-1) = 0"
   using mod_minus_right [of a 1] by simp
+
+lemma minus_mod_self2 [simp]: 
+  "(a - b) mod b = a mod b"
+  by (simp add: mod_diff_right_eq)
+
+lemma minus_mod_self1 [simp]: 
+  "(b - a) mod b = - a mod b"
+proof -
+  have "b - a = - a + b" by (simp add: diff_minus add.commute)
+  then show ?thesis by simp
+qed
 
 end
 
 
 subsection {* Generic numeral division with a pragmatic type class *}