proposition: Lemma invset_supperm s t : invset (supperm s t) = tclosure (invset s :|: invset t).
proof: Proof. rewrite /supperm perm_of_invsetK //. exact: is_invset_tclosureU (invsetP _) (invsetP _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype