[STATEMENT]
lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff p 0 \<noteq> (0::'a) \<Longrightarrow> degree (reflect_poly p) = degree p
[PROOF STEP]
by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)