proposition: Lemma noproots_cs p: (forall x, 0 <x -> ~~ root p x) -> 0 < lead_tail_coef p.
proof: Proof. move => h. have [pz |pnz]:= (eqVneq p 0); first by move: (h _ ltr01); rewrite pz root0. move: (mu_spec_supp pnz) => [q [pa pb pc pd pe]]. have: {in `[0, +oo[, (forall x, ~~ root q x)}. move=> x; rewrite in_itv/= andbT le0r; case/orP; first by move=>/eqP ->. by move /h; rewrite pa rootM negb_or => /andP []. move/sgp_pinftyP => ha; move: (ha 0). rewrite in_itv/= lexx /= => H. rewrite /lead_tail_coef pc pd pe - sgr_gt0 sgrM -/(sgp_pinfty q). by rewrite - horner_coef0 - H // - sgrM sgr_gt0 lt0r sqr_ge0 mulf_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)