fact: Definition infperm s t : 'S_n := maxperm * (supperm (maxperm * s) (maxperm * t)).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype