proposition: Lemma deg2_poly_lt0m x : r1 < x < r2 -> p.[x] < 0.
proof: Proof. move=> /andP[r1ltx xltr2]. have [dle0 | dgt0] := leP delta 0. by move: (lt_trans r1ltx xltr2); rewrite /r1 /r2 ler0_sqrtr// oppr0 ltxx. rewrite [p]deg2_poly_canonical// !hornerE/= -/a -/b -/c -/delta. rewrite pmulr_rlt0// subr_lt0 ltr_pdivlMr// xb4 -ltr_sqrt// sqrtr_sqr ltr_norml. by rewrite -ltrBlDr addrC -ltr_pdivrMr// r1ltx -ltrBrDr addrC -ltr_pdivlMr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)