proposition: Lemma size_cons_poly c p : size (cons_poly c p) = (if nilp p && (c == 0) then 0 else (size p).+1).
proof: Proof. by case: p => [[|c' s] _] //=; rewrite size_polyC; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)