proposition: Lemma dominant_eq m1 m2 : m1 \is dominant -> m2 \is dominant -> perm_eq m1 m2 -> m1 = m2.
proof: Proof. rewrite !unfold_in => /sorted_eq H{}/H H{}/H Heq. by apply/val_inj/val_inj; apply Heq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition