proposition: Lemma closed_nonrootP p : reflect (exists x, ~~ root p x) (p != 0).
proof: Proof. apply: (iffP idP) => [nz_p | [x]]; last first. by apply: contraNneq => ->; apply: root0. have [[x /rootP p1x0]|] := altP (closed_rootP (p - 1)). by exists x; rewrite -[p](subrK 1) /root hornerD p1x0 add0r hornerC oner_eq0. rewrite negbK => /size_poly1P[c _ /(canRL (subrK 1)) Dp]. by exists 0; rewrite Dp -raddfD polyC_eq0 rootC in nz_p *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)