proposition: Lemma size_addl p q : size p > size q -> size (p + q) = size p.
proof: Proof. move=> ltqp; rewrite -[+%R]/add_poly unlock size_poly_eq (maxn_idPl (ltnW _))//. by rewrite addrC nth_default ?simp ?nth_last //; case: p ltqp => [[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)