fact: Definition tinjval (s : 'S_m * 'S_n) := fun (x : 'I_(m + n)) => match split x with | inl a => unsplit (inl (s.1 a)) | inr a => unsplit (inr (s.2 a)) end.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg fingroup morphism perm gproduct) mathcomp(ssrnum matrix vector mxalgebra algC) mathcomp(classfun character mxrepresentation) tools ordcast partition sorted permcomp cycles cycletype permcent