proposition: Lemma mlastE (p : {mpoly R[n]}) (m : 'X_{1..n}) : m \in msupp p -> (forall m' : 'X_{1..n}, m' \in msupp p -> (m <= m')%O) -> mlast p = m.
proof: Proof. move=> mp le; apply/le_anti; rewrite mlast_lemc //=. by apply/le; rewrite mlast_supp // -msupp_eq0; case: msupp mp. 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