src/HOL/Decision_Procs/Cooper.thy

   then have ldcp: "0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) =l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
     by simp
   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) < (l div c) * 0"
     by (simp add: algebra_simps)

   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
     by simp
   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<le> (l div c) * 0"
     by (simp add: algebra_simps)

   then have ldcp: "0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
     by simp
   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) > (l div c) * 0"
     by (simp add: algebra_simps)

   then have ldcp: "0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) =l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    using mult_div_mod_eq [where a="l" and b="c"]
     by simp
   then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
     by simp
   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<ge> (l div c) * 0"

     by (simp add: zdiv_mono1[OF clel cp])
   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
     by simp
   then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
     by simp
   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0"

   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
     by simp
   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0"
     by (simp add: algebra_simps)

   then have ldcp:"0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
       (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
     by simp
   also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
     by (simp add: algebra_simps)

   then have ldcp: "0 < l div c"
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c* (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl:"c * (l div c) =l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    using mult_div_mod_eq [where a="l" and b="c"]
     by simp
   then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
       (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
     by simp
   also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"