mathlib3

e5befed7 - chore(data/polynomial/degree): golf some proofs, add simple lemmas (#5185)

chore(data/polynomial/degree): golf some proofs, add simple lemmas (#5185) * drop `polynomial.nat_degree_C_mul_X_pow_of_nonzero`; was a duplicate of `polynomial.nat_degree_C_mul_X_pow`; * golf the proof of `nat_degree_C_mul_X_pow_le`; * add more `simp` lemmas.