proposition: Lemma deg2_poly_noroot : reflect (forall x, ~~ root p x) (delta < 0).
proof: Proof. apply/(iffP idP) => [dlt0 x | /(_ r1)]. case: ltgtP aneq0 => [agt0 _|alt0 _|//]; rewrite rootE; last first. exact/lt0r_neq0/(deg2_poly_gt0 degp (ltW alt0)). rewrite -oppr_eq0 -hornerN. apply/lt0r_neq0/deg2_poly_gt0; rewrite ?size_opp ?coefN ?oppr_ge0 ?ltW//. by rewrite sqrrN -mulrA mulrNN mulrA. by rewrite ltNge; apply: contraNN => ?; apply: deg2_poly_root1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)