feat(data/polynomial/degree/trailing_degree): basic definitions and properties (#4113)
Adds trailing_degree, trailing_nat_degree, trailing_coeff and various lemmas add functionality to work with trailing coefficients
Co-authored-by: Johan Commelin <johan@commelin.net>