src/HOL/Algebra/Exponent.thy
changeset 24742 73b8b42a36b6
parent 23976 9a1859635978
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Thu Sep 27 17:28:05 2007 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu Sep 27 17:55:28 2007 +0200
     1.3 @@ -205,15 +205,10 @@
     1.4  apply (rule notnotD)
     1.5  apply (rule notI)
     1.6  apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
     1.7 -apply (drule_tac m = a in less_imp_le)
     1.8 +apply (drule less_imp_le [of a])
     1.9  apply (drule le_imp_power_dvd)
    1.10  apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
    1.11 -apply (frule_tac m = k in less_imp_le)
    1.12 -apply (drule_tac c = m in le_extend_mult, assumption)
    1.13 -apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
    1.14 -prefer 2 apply assumption
    1.15 -apply (rule dvd_refl [THEN dvd_mult2])
    1.16 -apply (drule_tac n = k in dvd_imp_le, auto)
    1.17 +apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less)
    1.18  done
    1.19  
    1.20  lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]