proposition: Lemma size_add p q : size (p + q) <= maxn (size p) (size q).
proof: Proof. by rewrite -[+%R]/add_poly unlock; apply: size_poly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)