proposition: Lemma all_roots_prod_XsubC p rs : size p = (size rs).+1 -> all (root p) rs -> uniq_roots rs -> p = lead_coef p *: \prod_(z <- rs) ('X - z%:P).
proof: Proof. move=> size_p /uniq_roots_prod_XsubC def_p Urs. case/def_p: Urs => q -> {p def_p} in size_p *. have [q0 | nz_q] := eqVneq q 0; first by rewrite q0 mul0r size_poly0 in size_p. have{q nz_q size_p} /size_poly1P[c _ ->]: size q == 1. rewrite -(eqn_add2r (size rs)) add1n -size_p. by rewrite size_Mmonic ?monic_prod_XsubC // size_prod_XsubC addnS. by rewrite lead_coef_Mmonic ?monic_prod_XsubC // lead_coefC mul_polyC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)