proposition: Lemma dec_factor_theorem (p : {poly F}) : {s : seq F & {q : {poly F} | p = q * \prod_(x <- s) ('X - x%:P) /\ (q != 0 -> forall x, ~~ root q x)}}.
proof: Proof. pose polyT (p : seq F) := (foldr (fun c f => f * 'X_0 + c%:T) (0%R)%:T p)%T. have eval_polyT (q : {poly F}) x : GRing.eval [:: x] (polyT q) = q.[x]. by rewrite /horner; elim: (val q) => //= ? ? ->. have [n] := ubnP (size p); elim: n => // n IHn in p *. have /decPcases /= := @satP F [::] ('exists 'X_0, polyT p == 0%T). case: ifP => [_ /sig_eqW[x]|_ noroot]; last first. exists [::], p; rewrite big_nil mulr1; split => // p_neq0 x. by apply/negP=> /rootP rpx; apply: noroot; exists x; rewrite eval_polyT. rewrite eval_polyT => /rootP/factor_theorem/sig_eqW[p1 ->]. have [->|nz_p1] := eqVneq p1 0; first by exists [::], 0; rewrite !mul0r eqxx. rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 => /IHn[s [q [-> irr_q]]]. by exists (rcons s x), q; rewrite -cats1 big_cat big_seq1 mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)