src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 46240 933f35c4e126
parent 41529 ba60efa2fd08
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 11:15:36 2012 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 16:30:54 2012 +0100
     1.3 @@ -723,8 +723,6 @@
     1.4          using t(1,2) m(2)[rule_format, OF tw] w0
     1.5          apply (simp only: )
     1.6          apply auto
     1.7 -        apply (rule mult_mono, simp_all add: norm_ge_zero)+
     1.8 -        apply (simp add: zero_le_mult_iff zero_le_power)
     1.9          done
    1.10        with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
    1.11        from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"