proposition: Lemma size_mulXn n p : p != 0 -> size (p * 'X^n) = (n + size p)%N.
proof: Proof. elim: n p => [p p_neq0| n IH p p_neq0]; first by rewrite mulr1. by rewrite exprS mulrA IH -?size_poly_eq0 size_mulX // addnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)