proposition: Lemma mleadcM p q : (p * q)@_(mlead p + mlead q) = mleadc p * mleadc q.
proof: Proof. have [->|nz_p] := eqVneq p 0; first by rewrite mleadc0 !mul0r mcoeff0. have [->|nz_q] := eqVneq q 0; first by rewrite mleadc0 !mulr0 mcoeff0. rewrite mpolyME (bigD1_seq (mlead p, mlead q)) /=; first last. + by rewrite allpairs_uniq => // -[? ?] []. + by rewrite allpairs_f// !mlead_supp. rewrite mcoeffD mcoeffZ mcoeffX eqxx mulr1. rewrite big_seq_cond raddf_sum /= big1 ?addr0 //. case=> m1 m2; rewrite in_allpairs//= -andbA; case/and3P. move=> m1_in_p m2_in_q ne_m_lc; rewrite mcoeffZ mcoeffX. move/msupp_le_mlead: m1_in_p; move/msupp_le_mlead: m2_in_q. rewrite le_eqVlt => /predU1P[m2E|]; last first. by move=> lt /lemc_lt_add /(_ lt) /lt_eqF ->; rewrite mulr0. move: ne_m_lc; rewrite m2E xpair_eqE eqxx andbT. rewrite le_eqVlt=> /negbTE -> /=; rewrite eqm_add2r. by move/lt_eqF=> ->; rewrite 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