feat(polynomial/derivative): tidy+new theorems (#12833)
Adds `iterate_derivative_eq_zero` and strengthens other results.
New theorems: `iterate_derivative_eq_zero`, `nat_degree_derivative_le`
Deleted: `derivative_lhom` - it is one already.
Misc: Turn a docstring into a comment
Everything else only got moved around + golfed, in order to weaken assumptions.
