src/HOL/Algebra/Exponent.thy
changeset 32946 22664da2923b
parent 32480 6c19da8e661a
child 35848 5443079512ea
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Thu Oct 15 16:15:22 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu Oct 15 17:04:45 2009 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4  apply (drule less_imp_le [of a])
     1.5  apply (drule le_imp_power_dvd)
     1.6  apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
     1.7 -apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
     1.8 +apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2 gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less nat_mult_commute not_add_less2 xt1(10))
     1.9  done
    1.10  
    1.11  lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]