proposition: Lemma all_pos_inv p: all_ge0 p -> inv p.
proof: Proof. move=> posp eps peps. move: (pol_cont ('X * p) 0 peps) => [e ep le]. have he := (half_gt0 ep). have hew:= (ltW he). exists (half e); split. by move=> y y0 ye; apply: all_pos_increasing. by move=> y y1 h h1; apply: all_pos_increasing => //; apply:(le_trans hew). have -> : half e* p.[half e] = ('X * p).[half e] - ('X * p).[0]. by rewrite !hornerM !hornerX mul0r subr0. have le1: `|half e - 0| < e by rewrite subr0 ger0_norm // half_ltx. by move /ler_normlP:(ltW(le _ le1)) => [_ ->]; rewrite he. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol