proposition: Lemma size_prod_XsubCe I rI (F : I -> R) (G : I -> nat) : size (\prod_(i <- rI) ('X - (F i)%:P)^+ (G i)) = (\sum_(i <- rI) (G i)).+1.
proof: Proof. elim: rI => [| i r /=]; rewrite ? big_nil ? size_poly1 // !big_cons. rewrite size_monicM ? monicXsubCe ? monic_neq0 // ?monic_prod_XsubCe //. by rewrite size_exp_XsubC => ->; rewrite addSn addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)