proposition: Lemma deg_le2_poly_le0 : (forall x, p.[x] <= 0) -> delta <= 0.
proof: Proof. move=> ple0; rewrite /delta -sqrrN -[c]opprK mulrN -mulNr -[-(4 * a)]mulrN. by rewrite -!coefN deg_le2_poly_ge0 ?size_opp// => x; rewrite hornerN oppr_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)