proposition: Lemma isantisym_mlead_rho : mlead p = rho.
proof: Proof. Proof using Hchar Hpanti Hphomog Hpn0. by apply/val_inj/val_inj; rewrite /= isantisym_mlead_iota rho_iota. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition