proposition: Lemma size_comp_poly p q : (size (p \Po q)).-1 = ((size p).-1 * (size q).-1)%N.
proof: Proof. have [-> | nz_p] := eqVneq p 0; first by rewrite comp_poly0 size_poly0. have [/size1_polyC-> | nc_q] := leqP (size q) 1. by rewrite comp_polyCr !size_polyC -!sub1b -!subnS muln0. have nz_q: q != 0 by rewrite -size_poly_eq0 -(subnKC nc_q). rewrite mulnC comp_polyE (polySpred nz_p) /= big_ord_recr /= addrC. rewrite size_addl size_scale ?lead_coef_eq0 ?size_exp //=. rewrite [ltnRHS]polySpred ?expf_neq0 // ltnS size_exp. rewrite (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _. rewrite (leq_trans (size_scale_leq _ _)) // polySpred ?expf_neq0 //. by rewrite size_exp -(subnKC nc_q) ltn_pmul2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)