proposition: Lemma poly_lim_infty p m : lead_coef p > 0 -> (size p > 1)%N -> exists n, forall x, x >= n -> p.[x] >= m.
proof: Proof. elim/poly_ind: p m => [| q c _] m; first by rewrite lead_coef0 ltxx. have [-> _|q_neq0] := eqVneq q 0. by rewrite mul0r add0r size_polyC ltnNge leq_b1. rewrite lead_coefDl ?size_mulX ?size_polyC // ?lead_coefMX; last first. by apply: (leq_trans (leq_b1 _)); rewrite size_poly_gt0. move=> lq_gt0; have [y Hy _] := poly_pinfty_gt_lc lq_gt0. pose z := (1 + (lead_coef q) ^-1 * (`|m| + `|c|)); exists (maxr y z) => x. have z_gt0 : 0 < z. by rewrite ltr_spaddl ?ltr01 ?mulr_ge0 ?invr_ge0 ?addr_ge0 // ?ltW. rewrite !hornerE le_maxl => /andP[/Hy Hq Hc]. apply: le_trans (_ : lead_coef q * z + c <= _); last first. rewrite ler_add2r (le_trans (_ : _ <= q.[x] * z)) // ?ler_pmul2r //. by rewrite ler_pmul2l // (lt_le_trans _ Hq). rewrite mulrDr mulr1 mulVKf ?gt_eqF // addrA -(addrA _ _ c) ler_paddr //. by rewrite -[c]opprK subr_ge0 normrN ler_norm. by rewrite ler_paddl ?ler_norm // ?ltW. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)