mathlib

356f889c - golf(data/polynomial/degree/definitions): golf three proofs (#15236)

golf(data/polynomial/degree/definitions): golf three proofs (#15236) Lemmas `degree_update_le`, `degree_nonneg_iff_ne_zero` and `degree_le_iff_coeff_zero` have shorter proofs. All three lemmas use the same axioms as they did before: ```lean propext quot.sound classical.choice ``` The golfing in `degree_le_iff_coeff_zero` is motivated by #15199, where the older version no longer compiles. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>