proposition: Lemma dvdp_prod_XsubC (I : Type) (r : seq I) (F : I -> R) p : p %| \prod_(i <- r) ('X - (F i)%:P) -> {m | p %= \prod_(i <- mask m r) ('X - (F i)%:P)}.
proof: Proof. elim: r => [|i r IHr] in p *. by rewrite big_nil dvdp1; exists nil; rewrite // big_nil -size_poly_eq1. rewrite big_cons dvdp_mul_XsubC root_factor_theorem -eqp_div_XsubC. case: eqP => [{2}-> | _] /IHr[m Dp]; last by exists (false :: m). by exists (true :: m); rewrite /= mulrC big_cons eqp_mul2l ?polyXsubC_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)