proposition: Lemma deg2_poly_gt0l x : x < r1 -> 0 < p.[x].
proof: Proof. move=> xltr1; have [? | dge0] := ltP delta 0; first exact: deg2_poly_gt0. have {}xltr1 : sqrt delta < - (x * (2 * a) + b). by rewrite ltrNr -ltrBrDr addrC -ltr_pdivlMr. rewrite [p]deg2_poly_canonical// -/a -/b -/c -/delta !hornerE/=. rewrite mulr_gt0// subr_gt0 ltr_pdivrMr// xb4 -sqrrN. rewrite -ltr_sqrt ?sqrtr_sqr ?(lt_le_trans xltr1) ?ler_norm//. by rewrite exprn_gt0 ?(le_lt_trans _ xltr1) ?sqrtr_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)