proposition: Lemma msizeM_proper p q : mleadc p * mleadc q != 0 -> msize (p * q) = (msize p + msize q).-1.
proof: Proof. have [->|nz_p ] := eqVneq p 0; first by rewrite mleadc0 mul0r eqxx. have [->|nz_q ] := eqVneq q 0; first by rewrite mleadc0 mulr0 eqxx. move=> h; rewrite -?[msize p]mlead_deg -?[msize q]mlead_deg //. rewrite !(addSn, addnS) -mdegD /= -mleadM_proper //. rewrite mlead_deg //; apply/negP; pose m := (mlead p + mlead q)%MM. move/eqP/(congr1 (mcoeff m)); rewrite mleadcM mcoeff0. by move/eqP; rewrite (negbTE h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg