proposition: Theorem factor_theorem p a : reflect (exists q, p = q * ('X - a%:P)) (root p a).
proof: Proof. apply: (iffP eqP) => [pa0 | [q ->]]; last first. by rewrite hornerM_comm /comm_poly hornerXsubC subrr ?simp. exists (\poly_(i < size p) horner_rec (drop i.+1 p) a). apply/polyP=> i; rewrite mulrBr coefB coefMX coefMC !coef_poly. apply: canRL (addrK _) _; rewrite addrC; have [le_p_i | lt_i_p] := leqP. rewrite nth_default // !simp drop_oversize ?if_same //. exact: leq_trans (leqSpred _). case: i => [|i] in lt_i_p *; last by rewrite ltnW // (drop_nth 0 lt_i_p). by rewrite drop1 /= -{}pa0 /horner; case: (p : seq R) lt_i_p. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)