proposition: Lemma size_prod_XsubC I rI (F : I -> R) : size (\prod_(i <- rI) ('X - (F i)%:P)) = (size rI).+1.
proof: Proof. elim: rI => [|i r /= <-]; rewrite ?big_nil ?size_poly1 // big_cons. rewrite size_monicM ?monicXsubC ?monic_neq0 ?monic_prod_XsubC //. by rewrite size_XsubC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)