src/HOL/Library/Polynomial.thy
changeset 56383 8e7052e9fda4
parent 55642 63beb38e9258
child 56544 b60d5d119489
     1.1 --- a/src/HOL/Library/Polynomial.thy	Thu Apr 03 17:56:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Apr 03 17:26:04 2014 +0100
     1.3 @@ -1747,12 +1747,9 @@
     1.4  lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
     1.5  apply (cases "p = 0", simp_all)
     1.6  apply (rule iffI)
     1.7 -apply (rule ccontr, simp)
     1.8 -apply (frule order_2 [where a=a], simp)
     1.9 -apply (simp add: poly_eq_0_iff_dvd)
    1.10 -apply (simp add: poly_eq_0_iff_dvd)
    1.11 -apply (simp only: order_def)
    1.12 -apply (drule not_less_Least, simp)
    1.13 +apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)
    1.14 +unfolding poly_eq_0_iff_dvd
    1.15 +apply (metis dvd_power dvd_trans order_1)
    1.16  done
    1.17  
    1.18