proposition: Lemma suppermPr s t : s <=R (supperm s t).
proof: Proof. rewrite !leperm_invset; rewrite invset_supperm /tclosure. apply/subsetP => /= [[i j] Hinv] /[!inE] /=. rewrite neq_ltn (DeltaP ((subsetP (invset_Delta s)) _ Hinv)) /=. by apply/connectP; exists [:: j]; rewrite //= inE Hinv /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype