src/HOL/Algebra/Exponent.thy

 apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
  prefer 2 apply (blast intro: dvd_mult2)
 apply (drule dvd_diffD1)
   apply assumption
- prefer 2 apply (blast intro: dvd_diff)
+ prefer 2 apply (blast intro: nat_dvd_diff)
 apply (drule gr0_implies_Suc, auto)
 done
 
 
 lemma r_le_a_forw:

 apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
  prefer 2 apply (blast intro: dvd_mult2)
 apply (drule dvd_diffD1)
   apply assumption
- prefer 2 apply (blast intro: dvd_diff)
+ prefer 2 apply (blast intro: nat_dvd_diff)
 apply (drule less_imp_Suc_add, auto)
 done
 
 lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]  
   ==> exponent p (p^a * m - k) = exponent p (p^a - k)"