proposition: Lemma isantisym_mlead_iota : mlead p = rev (iota 0 n) :> seq nat.
proof: Proof. Proof using Hchar Hpanti Hphomog Hpn0. move: Hphomog; rewrite binomial_sumn_iota => /dhomogP Hhomog. have Huniq := isantisym_msupp_uniq (mlead_supp Hpn0). rewrite -(revK (mlead p)) -{4}(size_tuple (mlead p)) -size_rev; congr rev. apply sorted_sumn_iotaE; first last. rewrite size_rev size_tuple sumn_rev sumnE -/(mdeg _). by rewrite (Hhomog _ (mlead_supp Hpn0)). rewrite ltn_sorted_uniq_leq rev_uniq Huniq /=. rewrite {Huniq Hhomog} rev_sorted. apply/(sorted2P 0%N) => // i j; rewrite size_tuple=> /andP[Hij Hj]. have H := mlead_antisym_sorted Hpanti. have /= := H (Ordinal (leq_ltn_trans Hij Hj)) (Ordinal Hj) Hij. by rewrite !(mnm_nth 0) /=; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition