proposition: Lemma odd_poly_root (p : {poly R}) : ~~ odd (size p) -> {x | root p x}.
proof: Proof. move=> size_p_even. have [->|p_neq0] := eqVneq p 0; first by exists 0; rewrite root0. pose b := cauchy_bound p. have [] := @ivt_sign p (-b) b; last by move=> x _; exists x. by rewrite ge0_cp // ?cauchy_bound_ge0. rewrite (sgp_minftyP (le_cauchy_bound p_neq0)) ?bound_in_itv //. rewrite (sgp_pinftyP (ge_cauchy_bound p_neq0)) ?bound_in_itv //. move: size_p_even; rewrite polySpred //= negbK /sgp_minfty -signr_odd => ->. by rewrite expr1 mulN1r sgrN mulNr -expr2 sqr_sg lead_coef_eq0 p_neq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)