proposition: Lemma deg2_poly_gt0 : 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 ltr_pdivlMr// mul0r oppr_gt0. apply: lt_le_trans (deg2_poly_min _). by rewrite deg2_poly_minE ltr_pdivlMr// mul0r oppr_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)