# HG changeset patch
# User huffman
# Date 1231861205 28800
# Node ID 6a46a13ce1f9cb4e1bf8c65236fedb801f639d56
# Parent  1851088a1f87c5b8392861debe7c78ab38276419
simplify proof of coeff_mult_degree_sum

diff -r 1851088a1f87 -r 6a46a13ce1f9 src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Tue Jan 13 06:57:08 2009 -0800
+++ b/src/HOL/Polynomial.thy	Tue Jan 13 07:40:05 2009 -0800
@@ -662,17 +662,7 @@
 lemma coeff_mult_degree_sum:
   "coeff (p * q) (degree p + degree q) =
    coeff p (degree p) * coeff q (degree q)"
- apply (simp add: coeff_mult)
- apply (subst setsum_diff1' [where a="degree p"])
-   apply simp
-  apply simp
- apply (subst setsum_0' [rule_format])
-  apply clarsimp
-  apply (subgoal_tac "degree p < a \<or> degree q < degree p + degree q - a")
-   apply (force simp add: coeff_eq_0)
-  apply arith
- apply simp
-done
+  by (induct p, simp, simp add: coeff_eq_0)
 
 instance poly :: (idom) idom
 proof