proposition: Lemma uniq_roots_prod_XsubC p rs : all (root p) rs -> uniq_roots rs -> exists q, p = q * \prod_(z <- rs) ('X - z%:P).
proof: Proof. elim: rs => [|z rs IHrs] /=; first by rewrite big_nil; exists p; rewrite mulr1. case/andP=> rpz rprs /andP[drs urs]; case: IHrs => {urs rprs}// q def_p. have [|q' def_q] := factor_theorem q z _; last first. by exists q'; rewrite big_cons mulrA -def_q. rewrite {p}def_p in rpz. elim/last_ind: rs drs rpz => [|rs t IHrs] /=; first by rewrite big_nil mulr1. rewrite all_rcons => /andP[/andP[/eqP czt Uzt] /IHrs{}IHrs]. rewrite -cats1 big_cat big_seq1 /= mulrA rootE hornerM_comm; last first. by rewrite /comm_poly hornerXsubC mulrBl mulrBr czt. rewrite hornerXsubC -opprB mulrN oppr_eq0 -(mul0r (t - z)). by rewrite (inj_eq (mulIr Uzt)) => /IHrs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)