mathlib3

b7e20ca0 - feat(data/polynomial/degree/definitions): two more `nat_degree_le` lemmas (#14098)

feat(data/polynomial/degree/definitions): two more `nat_degree_le` lemmas (#14098) This PR is similar to #14095. It proves the `le` version of `nat_degree_X_pow` and `nat_degree_monomial`. These lemmas are analogous to the existing `nat_degree_X_le` and `nat_degree_C_mul_X_pow_le`.