# HG changeset patch
# User wenzelm
# Date 1398801266 -7200
# Node ID e8cce2bd23e57e93ac80c19f18145dafc5f2320c
# Parent  a7c5c35b71258706e142ab9c2a09c956f0a4e8c1
tuned proofs;

diff -r a7c5c35b7125 -r e8cce2bd23e5 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 29 21:29:36 2014 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 29 21:54:26 2014 +0200
@@ -139,15 +139,16 @@
   from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
     by blast
   let ?k = " 1 + norm c + \<bar>r * m\<bar>"
-  have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
+  have kp: "?k > 0"
+    using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
   {
     fix z :: 'a
     assume H: "norm z \<le> r"
     from m H have th: "norm (poly cs z) \<le> m"
       by blast
-    from H have rp: "r \<ge> 0" using norm_ge_zero[of z]
-      by arith
-    have "norm (poly (pCons c cs) z) \<le> norm c + norm (z* poly cs z)"
+    from H have rp: "r \<ge> 0"
+      using norm_ge_zero[of z] by arith
+    have "norm (poly (pCons c cs) z) \<le> norm c + norm (z * poly cs z)"
       using norm_triangle_ineq[of c "z* poly cs z"] by simp
     also have "\<dots> \<le> norm c + r * m"
       using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
@@ -187,7 +188,8 @@
 
 lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
   apply (safe intro!: offset_poly_0)
-  apply (induct p, simp)
+  apply (induct p)
+  apply simp
   apply (simp add: offset_poly_pCons)
   apply (frule offset_poly_eq_0_lemma, simp)
   done
@@ -278,7 +280,8 @@
       by presburger+
     with IH[rule_format, of m] obtain z where z: "?P z m"
       by blast
-    from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
+    from z have "?P (csqrt z) n"
+      by (simp add: m power_mult csqrt)
     then have "\<exists>z. ?P z n" ..
   }
   moreover
@@ -288,16 +291,25 @@
       using b by (simp add: norm_divide)
     from o have "\<exists>m. n = Suc (2 * m)"
       by presburger+
-    then obtain m where m: "n = Suc (2*m)"
+    then obtain m where m: "n = Suc (2 * m)"
       by blast
     from unimodular_reduce_norm[OF th0] o
     have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
-      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
-      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp)
+      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1")
+      apply (rule_tac x="1" in exI)
+      apply simp
+      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1")
+      apply (rule_tac x="-1" in exI)
+      apply simp
       apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
-      apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
-      apply (rule_tac x="- ii" in exI, simp add: m power_mult)
-      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
+      apply (cases "even m")
+      apply (rule_tac x="ii" in exI)
+      apply (simp add: m power_mult)
+      apply (rule_tac x="- ii" in exI)
+      apply (simp add: m power_mult)
+      apply (cases "even m")
+      apply (rule_tac x="- ii" in exI)
+      apply (simp add: m power_mult)
       apply (auto simp add: m power_mult)
       apply (rule_tac x="ii" in exI)
       apply (auto simp add: m power_mult)
@@ -329,7 +341,7 @@
 text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
 
 lemma metric_bound_lemma: "cmod (x - y) \<le> \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
-  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
+  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
   unfolding cmod_def by simp
 
 lemma bolzano_weierstrass_complex_disc:
@@ -374,12 +386,12 @@
 
   from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
     by blast
-  then have x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
+  then have x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Re (s (f n)) - x\<bar> < r"
     unfolding LIMSEQ_iff real_norm_def .
 
   from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
     by blast
-  then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
+  then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Im (s (f (g n))) - y\<bar> < r"
     unfolding LIMSEQ_iff real_norm_def .
   let ?w = "Complex x y"
   from f(1) g(1) have hs: "subseq ?h"
@@ -387,10 +399,12 @@
   {
     fix e :: real
     assume ep: "e > 0"
-    then have e2: "e/2 > 0" by simp
+    then have e2: "e/2 > 0"
+      by simp
     from x[rule_format, OF e2] y[rule_format, OF e2]
     obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2"
-      and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
+      and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2"
+      by blast
     {
       fix n
       assume nN12: "n \<ge> N1 + N2"
@@ -400,7 +414,8 @@
       have "cmod (s (?h n) - ?w) < e"
         using metric_bound_lemma[of "s (f (g n))" ?w] by simp
     }
-    then have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast
+    then have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e"
+      by blast
   }
   with hs show ?thesis by blast
 qed
@@ -514,7 +529,8 @@
       let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
       {
         assume e: "?e > 0"
-        then have e2: "?e/2 > 0" by simp
+        then have e2: "?e/2 > 0"
+          by simp
         from poly_cont[OF e2, of z p] obtain d where
             d: "d > 0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2"
           by blast
@@ -541,25 +557,25 @@
         have ath: "\<And>m x e::real. m \<le> x \<Longrightarrow> x < m + e \<Longrightarrow> \<bar>x - m\<bar> < e"
           by arith
         from s1m[OF g(1)[rule_format]] have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
-        from seq_suble[OF fz(1), of "N1+N2"]
+        from seq_suble[OF fz(1), of "N1 + N2"]
         have th00: "real (Suc (N1 + N2)) \<le> real (Suc (f (N1 + N2)))"
           by simp
         have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1 + N2)) > 0"
           using N2 by auto
         from frac_le[OF th000 th00]
-        have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))"
+        have th00: "?m + 1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))"
           by simp
         from g(2)[rule_format, of "f (N1 + N2)"]
         have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
         from order_less_le_trans[OF th01 th00]
-        have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
+        have th32: "cmod (poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
         from N2 have "2/?e < real (Suc (N1 + N2))"
           by arith
         with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
         have "?e/2 > 1/ real (Suc (N1 + N2))"
           by (simp add: inverse_eq_divide)
         with ath[OF th31 th32]
-        have thc1: "\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
+        have thc1: "\<bar>cmod (poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
           by arith
         have ath2: "\<And>a b c m::real. \<bar>a - b\<bar> \<le> c \<Longrightarrow> \<bar>b - m\<bar> \<le> \<bar>a - m\<bar> + c"
           by arith
@@ -593,7 +609,7 @@
 lemma cispi: "cis pi = -1"
   by (simp add: cis_def)
 
-lemma "(rcis (sqrt (abs r)) ((pi + a)/2))\<^sup>2 = rcis (- abs r) a"
+lemma "(rcis (sqrt (abs r)) ((pi + a) / 2))\<^sup>2 = rcis (- abs r) a"
   unfolding power2_eq_square
   apply (simp add: rcis_mult add_divide_distrib)
   apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
@@ -607,16 +623,21 @@
   shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
   using ex
 proof (induct p arbitrary: a d)
+  case 0
+  then show ?case by simp
+next
   case (pCons c cs a d)
-  {
-    assume H: "cs \<noteq> 0"
+  show ?case
+  proof (cases "cs = 0")
+    case False
     with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)"
       by blast
     let ?r = "1 + \<bar>r\<bar>"
     {
-      fix z::'a
+      fix z :: 'a
       assume h: "1 + \<bar>r\<bar> \<le> norm z"
-      have r0: "r \<le> norm z" using h by arith
+      have r0: "r \<le> norm z"
+        using h by arith
       from r[rule_format, OF r0] have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)"
         by arith
       from h have z1: "norm z \<ge> 1"
@@ -625,21 +646,18 @@
       have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
         unfolding norm_mult by (simp add: algebra_simps)
       from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
-      have th2: "norm(z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
+      have th2: "norm (z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
         by (simp add: algebra_simps)
-      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)" by arith
+      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
+        by arith
     }
-    then have ?case by blast
-  }
-  moreover
-  {
-    assume cs0: "\<not> (cs \<noteq> 0)"
+    then show ?thesis by blast
+  next
+    case True
     with pCons.prems have c0: "c \<noteq> 0"
       by simp
-    from cs0 have cs0': "cs = 0"
-      by simp
     {
-      fix z::'a
+      fix z :: 'a
       assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
       from c0 have "norm c > 0"
         by simp
@@ -650,12 +668,11 @@
       from norm_diff_ineq[of "z * c" a] have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
         by (simp add: algebra_simps)
       from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
-        using cs0' by simp
+        using True by simp
     }
-    then have ?case  by blast
-  }
-  ultimately show ?case by blast
-qed simp
+    then show ?thesis by blast
+  qed
+qed
 
 text {* Hence polynomial's modulus attains its minimum somewhere. *}
 lemma poly_minimum_modulus: "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
@@ -691,13 +708,12 @@
 qed
 
 text{* Constant function (non-syntactic characterization). *}
-definition "constant f = (\<forall>x y. f x = f y)"
+definition "constant f \<longleftrightarrow> (\<forall>x y. f x = f y)"
 
 lemma nonconstant_length: "\<not> constant (poly p) \<Longrightarrow> psize p \<ge> 2"
   by (induct p) (auto simp: constant_def psize_def)
 
-lemma poly_replicate_append:
-  "poly (monom 1 n * p) (x::'a::{comm_ring_1}) = x^n * poly p x"
+lemma poly_replicate_append: "poly (monom 1 n * p) (x::'a::comm_ring_1) = x^n * poly p x"
   by (simp add: poly_monom)
 
 text {* Decomposition of polynomial, skipping zero coefficients
@@ -705,8 +721,7 @@
 
 lemma poly_decompose_lemma:
   assumes nz: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly p z = (0::'a::idom))"
-  shows "\<exists>k a q. a \<noteq> 0 \<and> Suc (psize q + k) = psize p \<and>
-    (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
+  shows "\<exists>k a q. a \<noteq> 0 \<and> Suc (psize q + k) = psize p \<and> (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   unfolding psize_def
   using nz
 proof (induct p)
@@ -746,7 +761,7 @@
 next
   case (pCons c cs)
   {
-    assume C:"\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
+    assume C: "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
     {
       fix x y
       from C have "poly (pCons c cs) x = poly (pCons c cs) y"
@@ -793,13 +808,16 @@
       by blast
     {
       assume h: "constant (poly q)"
-      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
+      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x"
+        by auto
       {
         fix x y
-        from th have "?p x = poly q (x - c)" by auto
+        from th have "?p x = poly q (x - c)"
+          by auto
         also have "\<dots> = poly q (y - c)"
           using h unfolding constant_def by blast
-        also have "\<dots> = ?p y" using th by auto
+        also have "\<dots> = ?p y"
+          using th by auto
         finally have "?p x = ?p y" .
       }
       with less(2) have False
@@ -833,7 +851,8 @@
           using qr[rule_format, of y] by simp
         finally have "poly q x = poly q y" .
       }
-      with qnc have False unfolding constant_def by blast
+      with qnc have False
+        unfolding constant_def by blast
     }
     then have rnc: "\<not> constant (poly ?r)"
       unfolding constant_def by blast
@@ -871,7 +890,8 @@
         by simp
       have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
         unfolding constant_def poly_pCons poly_monom
-        using kas(1) apply simp
+        using kas(1)
+        apply simp
         apply (rule exI[where x=0])
         apply (rule exI[where x=1])
         apply simp
@@ -884,8 +904,8 @@
         using kas(2) by (cases k) (auto simp add: algebra_simps)
       from poly_bound_exists[of "cmod w" s] obtain m where
         m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
-      have w0: "w \<noteq> 0" using kas(2) w
-        by (auto simp add: power_0_left)
+      have w0: "w \<noteq> 0"
+        using kas(2) w by (auto simp add: power_0_left)
       from w have "(1 + w ^ k * a) - 1 = 0 - 1"
         by simp
       then have wm1: "w^k * a = - 1"
@@ -981,24 +1001,30 @@
           case False
           from poly_bound_exists[of 1 ds] obtain m where
             m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
-          have dm: "cmod d / m > 0" using False m(1) by (simp add: field_simps)
+          have dm: "cmod d / m > 0"
+            using False m(1) by (simp add: field_simps)
           from real_lbound_gt_zero[OF dm zero_less_one] obtain x where
             x: "x > 0" "x < cmod d / m" "x < 1" by blast
           let ?x = "complex_of_real x"
-          from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
+          from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1"
+            by simp_all
           from pCons.prems[rule_format, OF cx(1)]
-          have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
+          have cth: "cmod (?x*poly ds ?x) = cmod d"
+            by (simp add: eq_diff_eq[symmetric])
           from m(2)[rule_format, OF cx(2)] x(1)
           have th0: "cmod (?x*poly ds ?x) \<le> x*m"
             by (simp add: norm_mult)
-          from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
-          with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
-          with cth show ?thesis by blast
+          from x(2) m(1) have "x * m < cmod d"
+            by (simp add: field_simps)
+          with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d"
+            by auto
+          with cth show ?thesis
+            by blast
         qed
       qed
     }
-    then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems False
-      by blast
+    then have nc: "\<not> constant (poly (pCons c cs))"
+      using pCons.prems False by blast
     from fundamental_theorem_of_algebra[OF nc] show ?thesis .
   qed
 qed
@@ -1053,12 +1079,17 @@
           from sne kpn have k: "k \<noteq> 0" by simp
           let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
           have "q ^ n = p * ?w"
-            apply (subst r, subst s, subst kpn)
+            apply (subst r)
+            apply (subst s)
+            apply (subst kpn)
             using k oop [of a]
-            apply (subst power_mult_distrib, simp)
-            apply (subst power_add [symmetric], simp)
+            apply (subst power_mult_distrib)
+            apply simp
+            apply (subst power_add [symmetric])
+            apply simp
             done
-          then have ?ths unfolding dvd_def by blast
+          then have ?ths
+            unfolding dvd_def by blast
         }
         moreover
         {
@@ -1076,25 +1107,33 @@
                 from h[unfolded xa poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
                   by (rule dvdE)
                 have "p = [:- a, 1:] ^ (Suc ?op) * u"
-                  by (subst s, subst u, simp only: power_Suc mult_ac)
-                with ap(2)[unfolded dvd_def] have False by blast
+                  apply (subst s)
+                  apply (subst u)
+                  apply (simp only: power_Suc mult_ac)
+                  done
+                with ap(2)[unfolded dvd_def] have False
+                  by blast
               }
               note xa = this
-              from h have "poly p x = 0" by (subst s) simp
-              with pq0 have "poly q x = 0" by blast
+              from h have "poly p x = 0"
+                by (subst s) simp
+              with pq0 have "poly q x = 0"
+                by blast
               with r xa have "poly r x = 0"
                 by auto
             }
             note impth = this
             from IH[rule_format, OF dsn, of s r] impth ds0
-            have "s dvd (r ^ (degree s))" by blast
+            have "s dvd (r ^ (degree s))"
+              by blast
             then obtain u where u: "r ^ (degree s) = s * u" ..
             then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
               by (simp only: poly_mult[symmetric] poly_power[symmetric])
             let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
             from oop[of a] dsn have "q ^ n = p * ?w"
               apply -
-              apply (subst s, subst r)
+              apply (subst s)
+              apply (subst r)
               apply (simp only: power_mult_distrib)
               apply (subst mult_assoc [where b=s])
               apply (subst mult_assoc [where a=u])
@@ -1102,7 +1141,8 @@
               apply (subst u [symmetric])
               apply (simp add: mult_ac power_add [symmetric])
               done
-            then have ?ths unfolding dvd_def by blast
+            then have ?ths
+              unfolding dvd_def by blast
         }
         ultimately have ?ths by blast
       }
@@ -1154,7 +1194,8 @@
       from k dp have "q ^ (degree p) = p * [:1/k:]"
         by (simp add: one_poly_def)
       then have th2: "p dvd (q ^ (degree p))" ..
-      from th1 th2 pe have ?thesis by blast
+      from th1 th2 pe have ?thesis
+        by blast
     }
     moreover
     {
@@ -1181,7 +1222,7 @@
   ultimately show ?thesis by blast
 qed
 
-text{* Useful lemma *}
+text {* Useful lemma *}
 
 lemma constant_degree:
   fixes p :: "'a::{idom,ring_char_0} poly"
@@ -1210,7 +1251,7 @@
   shows "degree p \<le> degree q \<or> q = 0"
   by (metis dvd_imp_degree_le pq)
 
-(* Arithmetic operations on multivariate polynomials.                        *)
+text {* Arithmetic operations on multivariate polynomials. *}
 
 lemma mpoly_base_conv:
   fixes x :: "'a::comm_ring_1"
@@ -1232,7 +1273,7 @@
 
 lemma poly_cancel_eq_conv:
   fixes x :: "'a::field"
-  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (y = 0) = (a * y - b * x = 0)"
+  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> y = 0 \<longleftrightarrow> a * y - b * x = 0"
   by auto
 
 lemma poly_divides_pad_rule:
@@ -1300,8 +1341,8 @@
   by simp_all
 
 lemma basic_cqe_conv2:
-  assumes l:"p \<noteq> 0"
-  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex))"
+  assumes l: "p \<noteq> 0"
+  shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
 proof -
   {
     fix h t
@@ -1320,7 +1361,7 @@
 lemma basic_cqe_conv3:
   fixes p q :: "complex poly"
   assumes l: "p \<noteq> 0"
-  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> ((pCons a p) dvd (q ^ psize p))"
+  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> (pCons a p) dvd (q ^ psize p)"
 proof -
   from l have dp: "degree (pCons a p) = psize p"
     by (simp add: psize_def)