mathlib

f6178629 - feat(data/polynomial/degree/lemmas): two lemmas about `nat_degree`s of sums (#14100)

feat(data/polynomial/degree/lemmas): two lemmas about `nat_degree`s of sums (#14100) Suppose that `f, g` are polynomials. If both `nat_degree (f + g)` and `nat_degree` of one of them are bounded by `n`, then `nat_degree` of the other is also bounded by `n`.