src/HOL/Decision_Procs/Commutative_Ring.thy

--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -60,6 +60,9 @@
 
 text {* Defining the basic ring operations on normalized polynomials *}
 
+lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
+  by (cases p) simp_all
+
 function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<oplus>" 65)
 where
   "Pc a \<oplus> Pc b = Pc (a + b)"