Theorem filter.eventually_eq.div'

chore(order/filter/basic): rename using the zero subscript convention for groups with zero (#12952)

feat(analysis): prove that a polynomial function is equivalent to its leading term along at_top, and consequences (#5354) …