src/HOL/Algebra/UnivPoly.thy
changeset 26934 c1ae80a58341
parent 26202 51f8a696cd8d
child 27611 2c01c0bdb385
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sat May 17 21:46:24 2008 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sat May 17 23:37:07 2008 +0200
     1.3 @@ -483,6 +483,7 @@
     1.4    proof (cases "k = Suc n")
     1.5      case True show ?thesis
     1.6      proof -
     1.7 +      fix m
     1.8        from True have less_add_diff:
     1.9          "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
    1.10        from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp