proposition: Lemma mleadcMW p q (mp mq : 'X_{1..n}) : (mlead p <= mp)%O -> (mlead q <= mq)%O -> (p * q)@_(mp + mq)%MM = p@_mp * q@_mq.
proof: Proof. case: (boolP ((mlead p < mp) || (mlead q < mq)))%O; last first. by case: ltgtP => // <-; case: ltgtP => // <- _ _ _; apply: mleadcM. move=> lt_lm lep leq; have lt_lmD: ((mlead p + mlead q)%MM < (mp + mq)%MM)%O. by case/orP: lt_lm=> lt; [apply/ltmc_le_add | apply/lemc_lt_add]. move/(le_lt_trans (mleadM_le p q))/mcoeff_gt_mlead: lt_lmD. by case/orP: lt_lm=> /mcoeff_gt_mlead ->; rewrite ?(mul0r, mulr0). 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