proposition: Lemma ltm_mleadD p (q := p - p@_(mlead p) *: 'X_[mlead p]) : p != 0 -> q != 0 -> (mlead q < mlead p)%O.
proof: Proof. move=> Zp Zq; have: mlead q \in (rem (mlead p) (msupp p)). by rewrite -(perm_mem (msupp_rem p _)) // mlead_supp. rewrite (rem_filter _ (msupp_uniq p)) mem_filter /= => /andP[h]. suff: (mlead q <= mlead p)%O by rewrite le_eqVlt (negPf h). apply: le_trans (mleadB_le _ _) _; rewrite leUx lexx /=. by rewrite (le_trans (mleadZ_le _ _)) // mleadXm. 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