The last step does not follow from your th05
. The problem is that you seem to want to unify (SOME y. y∈{x∷nat. x ≤ n})
with the bound variable i
. However, in HOL (SOME y. y∈{x∷nat. x ≤ n})
has a single value that depends only on n
and not on i
. Furthermore, you don't get to choose the value; a theorem using SOME
is not the same as a theorem with a universally quantified variable.
My advice is to avoid using SOME
altogether, and instead try to prove a generalization of your theorem first:
lemma degree_setsum_smaller:
"finite A ⟹ ∀x∈A. degree (f x) ≤ n ⟹ degree (∑x∈A. f x) ≤ n"
You should be able to prove degree_setsum_smaller
by induction over A
(use induct rule: finite_induct
), and then use it to prove degree_poly_smaller
. Lemma degree_add_le
from the polynomial library should be useful.