proposition: Lemma deg2_poly_ge0r x : r2 <= x -> 0 <= p.[x].
proof: Proof. rewrite le_eqVlt => /orP[/eqP<-|xgtr2]; last exact/ltW/deg2_poly_gt0r. have [dge0|dlt0] := leP 0 delta; last by apply: deg2_poly_ge0 => //; apply: ltW. by rewrite le_eqVlt (rootP (deg2_poly_root2 dge0)) eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)