proposition: Lemma deg_le2_poly_delta_ge0 : 0 <= a -> (forall x, 0 <= p.[x]) -> delta <= 0.
proof: Proof. move=> age0 pge0; move: degp; rewrite leq_eqVlt => /orP[/eqP|] degp'. exact/(Real.deg2_poly_ge0 degp' age0). have a0 : a = 0 by rewrite /a nth_default. rewrite /delta a0 mulr0 mul0r subr0 exprn_even_le0//=. have [//|/eqP nzb] := eqP; move: (pge0 ((- 1 - c) / b)). have -> : p = b *: 'X + c%:P. apply/polyP => + /[!coefE] => -[|[|i]] /=; rewrite !Monoid.simpm//. by rewrite nth_default// -ltnS (leq_trans degp'). by rewrite !hornerE/= mulrAC mulfV// mul1r subrK ler0N1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)