src/HOL/NumberTheory/Int2.thy

 
 subsection {* Useful lemmas about dvd and powers *}
 
 lemma zpower_zdvd_prop1:
   "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
-  by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
+  by (induct n) (auto simp add: dvd_mult2 [of p y])
 
 lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m"
 proof -
   assume "n dvd m"
   then have "~(0 < m & m < n)"

     "zprime p \<Longrightarrow> p dvd ((y::int) ^ n) \<Longrightarrow> 0 < n \<Longrightarrow> p dvd y"
   apply (induct n)
    apply simp
   apply (frule zprime_zdvd_zmult_better)
    apply simp
-  apply force
+  apply (force simp del:dvd_mult)
   done
 
 lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
 proof -
   assume "0 < z" then have modth: "x mod z \<ge> 0" by simp

 
 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
   by (auto simp add: zcong_def)
 
 lemma zcong_id: "[m = 0] (mod m)"
-  by (auto simp add: zcong_def zdvd_0_right)
+  by (auto simp add: zcong_def)
 
 lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
   by (auto simp add: zcong_refl zcong_zadd)
 
 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"