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