# Zulip Chat Archive

## Stream: triage

### Topic: PR #4069: added statements for trailing_degree, nat_trail...

#### Random Issue Bot (Feb 15 2021 at 14:20):

Today I chose PR 4069 for discussion!

**added statements for trailing_degree, nat_trailing_degree, trailing_coeff,... Many proofs are missing!**

Created by @**damiano** (@adomani) on 2020-09-08

Labels: help wanted, incomplete, needs-documentation

Is this PR still relevant? Any recent updates? Anyone making progress?

#### Damiano Testa (Feb 15 2021 at 14:35):

The lemmas in this PR are adaptations of the lemmas that existed at the time for the `leading_coefficient`

of a polynomial, but not for the `trailing_coefficient`

. Now, with the definition of `reflect`

most of these lemmas can, in theory, be proved by reducing statements about the `trailing_degree`

of `f`

to statements about the `leading_coefficient`

of `reflect f`

. The missing ingredient is a proof that leading and trailing coefficients are exchanged by `reflect`

. An earlier proof of this fact did not use `dual_order`

and did not make into mathlib. I was not able to make the version with `order_dual`

to work, so I am stuck and stopped thinking about this.

The lemma that I feel should be in mathlib is the statement that the trailing degree of a product is the product of the trailing degrees (with some assumptions). There have been many refactors, since I last checked: I doubt that this result is in mathlib, but if it is, then closing this PR would be fine for me!

Last updated: May 09 2021 at 16:20 UTC