proposition: Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.
proof: Proof. rewrite -[n]card_ord -prodr_const -big_filter size_prod_XsubC. by have [e _ _ [_ ->]] := big_enumP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)