proposition: Lemma size_comp_poly2 p q : size q = 2 -> size (p \Po q) = size p.
proof: Proof. move=> sq2; have [->|pN0] := eqVneq p 0; first by rewrite comp_polyC. by rewrite polySpred ?size_comp_poly ?comp_poly_eq0 ?sq2 // muln1 polySpred. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)