proposition: Lemma mlast_lemc m p : m \in msupp p -> (mlast p <= m)%O.
proof: Proof. rewrite /mlast -nth0; set s := sort _ _. have: perm_eq s (msupp p) by apply/permEl/perm_sort. have: sorted <=%O%O s by apply/sort_sorted/le_total. case: s => /= [_|m' s srt_s]; first rewrite perm_sym. by move/perm_small_eq=> -> //. move/perm_mem => <-; rewrite in_cons => /predU1P[->//|]. elim: s m' srt_s => //= m'' s ih m' /andP[le_mm' /ih {}ih]. by rewrite in_cons => /predU1P[->//|/ih /(le_trans le_mm')]. 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