src/HOL/Library/Poly_Deriv.thy
changeset 58199 5fbe474b5da8
parent 56383 8e7052e9fda4
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Poly_Deriv.thy	Sun Sep 07 09:49:01 2014 +0200
     1.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Sun Sep 07 09:49:05 2014 +0200
     1.3 @@ -130,8 +130,13 @@
     1.4    shows "n = order a p"
     1.5  unfolding Polynomial.order_def
     1.6  apply (rule Least_equality [symmetric])
     1.7 -apply (rule assms)
     1.8 -by (metis assms not_less_eq_eq power_le_dvd)
     1.9 +apply (fact assms)
    1.10 +apply (rule classical)
    1.11 +apply (erule notE)
    1.12 +unfolding not_less_eq_eq
    1.13 +using assms(1) apply (rule power_le_dvd)
    1.14 +apply assumption
    1.15 +done
    1.16  
    1.17  lemma lemma_order_pderiv1:
    1.18    "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +