proposition: Lemma mnm_perm m1 m2 : perm_eq m1 m2 -> {s : 'S_n | m1 == m2 # s}.
proof: Proof. move=> Hperm; apply sigW; move: Hperm => /tuple_permP[s /val_inj Hs] /=. by exists s; apply/eqP; apply val_inj => /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition