proposition: Lemma size_Mmonic p q : p != 0 -> q \is monic -> size (p * q) = (size p + size q).-1.
proof: Proof. move=> nz_p /monicP mon_q. by rewrite size_proper_mul // mon_q mulr1 lead_coef_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)