proposition: Lemma size_comp_poly_leq p q : size (p \Po q) <= ((size p).-1 * (size q).-1).+1.
proof: Proof. rewrite comp_polyE (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _. rewrite (leq_trans (size_scale_leq _ _)) // (leq_trans (size_exp_leq _ _)) //. by rewrite ltnS mulnC leq_mul // -{2}(subnKC (valP i)) leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)