lemmas about coeff for `compute_degree` (#15694)
This PR proves 5 lemmas about `coeff`s of polynomials under products, multiplications, sums and differences.
I also moved an already existing `ring` lemma to a previously non-existing section on `ring`.
These lemmas are useful for the `compute_degree` tactic of #15691.
