proposition: Lemma suppermPl s t : t <=R (supperm s t).
proof: Proof. by rewrite suppermC; exact: suppermPr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype