proposition: Lemma suppermC s t : supperm s t = supperm t s.
proof: Proof. by apply: invset_inj; rewrite [RHS]invset_supperm [LHS]invset_supperm setUC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype