proposition: Lemma deg2_poly_le0 : reflect (forall x, p.[x] <= 0) (delta <= 0).
proof: Proof. rewrite -deltaN; apply/(iffP (deg2_poly_ge0 _ _)); rewrite ?coefN ?oppr_ge0//. - by move=> ge0 x; rewrite -oppr_ge0 -hornerN ge0. - by move=> le0 x; rewrite hornerN oppr_ge0 le0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)