proposition: Lemma deg_le2_poly_ge0 : (forall x, 0 <= p.[x]) -> delta <= 0.
proof: Proof. have [age0|alt0] := leP 0 a; first exact: deg_le2_poly_delta_ge0. move=> pge0; move: degp; rewrite leq_eqVlt => /orP[/eqP|] degp'; last first. by move: alt0; rewrite /a nth_default ?ltxx. have [//|dge0] := leP delta 0. pose r1 := (- b - sqrt delta) / (2 * a). pose r2 := (- b + sqrt delta) / (2 * a). pose x0 := Num.max (r1 + 1) (r2 + 1). move: (pge0 x0); rewrite (Real.deg2_poly_factor degp' (ltW dge0)). rewrite !hornerE/= -mulrA nmulr_rge0// leNgt => /negbTE<-. by apply: mulr_gt0; rewrite subr_gt0 lt_max ltrDl ltr01 ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)