proposition: Lemma eltrpK : involutive eltrp.
proof: Proof. by move=> [u v]; rewrite /eltrp !eltrK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition