proposition: Lemma lead_coefDl p q : size p > size q -> lead_coef (p + q) = lead_coef p.
proof: Proof. move=> ltqp; rewrite /lead_coef coefD size_addl //. by rewrite addrC nth_default ?simp // -ltnS (ltn_predK ltqp). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)