Theorem polynomial.div_tendsto_at_top_of_degree_gt'

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