Commit 2022-05-26 13:56 70e784d0

feat(data/polynomial/*): (p * q).trailing_degree = p.trailing_degree + q.trailing_degree (#14384) We already had a nat_trailing_degree_mul lemma, but this PR does things properly, following the analogous results for degree. In particular, we now have some useful intermediate results that do not assume no_zero_divisors.