mathlib

189e5d13 - feat(data/polynomial/degree/trailing_degree): The trailing degree of a product is at least the sum of the trailing degrees (#14253)

feat(data/polynomial/degree/trailing_degree): The trailing degree of a product is at least the sum of the trailing degrees (#14253) This PR adds lemmas for `nat_trailing_degree` analogous to `degree_mul_le` and `nat_degree_mul_le`.