[STATEMENT]
lemma fls_subdegree_deriv':
  fixes   f :: "'a::ring_1_no_zero_divisors fls"
  assumes "(of_int (fls_subdegree f) :: 'a) \<noteq> 0"
  shows   "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fls_subdegree (fls_deriv f) = fls_subdegree f - 1
[PROOF STEP]
using   assms nth_fls_subdegree_zero_iff[of f]
[PROOF STATE]
proof (prove)
using this:
of_int (fls_subdegree f) \<noteq> (0::'a)
(f $$ fls_subdegree f = (0::'a)) = (f = 0)

goal (1 subgoal):
 1. fls_subdegree (fls_deriv f) = fls_subdegree f - 1
[PROOF STEP]
by      (auto intro: fls_deriv_subdegree')