proposition: Lemma size_proper_mul p q : lead_coef p * lead_coef q != 0 -> size (p * q) = (size p + size q).-1.
proof: Proof. apply: contraNeq; rewrite mul_lead_coef eqn_leq size_mul_leq -ltnNge => lt_pq. by rewrite nth_default // -subn1 -(leq_add2l 1) -leq_subLR leq_sub2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)