proposition: Lemma size_MXaddC p c : size (p * 'X + c%:P) = (if (p == 0) && (c == 0) then 0 else (size p).+1).
proof: Proof. by rewrite -cons_poly_def size_cons_poly nil_poly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)