proposition: Lemma closed_rootP p : reflect (exists x, root p x) (size p != 1).
proof: Proof. have [-> | nz_p] := eqVneq p 0. by rewrite size_poly0; left; exists 0; rewrite root0. rewrite neq_ltn [in _ < 1]polySpred //=. apply: (iffP idP) => [p_gt1 | [a]]; last exact: root_size_gt1. pose n := (size p).-1; have n_gt0: n > 0 by rewrite -ltnS -polySpred. have [a Dan] := closedF (fun i => - p`_i / lead_coef p) n_gt0. exists a; apply/rootP; rewrite horner_coef polySpred // big_ord_recr /= -/n. rewrite {}Dan mulr_sumr -big_split big1 //= => i _. by rewrite -!mulrA mulrCA mulNr mulVKf ?subrr ?lead_coef_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)