proposition: Lemma deg2_poly_ge0 : reflect (forall x, 0 <= p.[x]) (delta <= 0).
proof: Proof. apply/(iffP idP) => [dlt0 x | /(_ (- b / (2 * a)))]; last first. by rewrite deg2_poly_minE ler_pdivlMr// mul0r oppr_ge0. apply: le_trans (deg2_poly_min _). by rewrite deg2_poly_minE ler_pdivlMr// mul0r 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)