proposition: Lemma porbits_tinj s : porbits (tinj s) = [set (@lshift m n) @: x | x : {set 'I_m} in porbits s.1] :|: [set (@rshift m n) @: x | x : {set 'I_n} in porbits s.2].
proof: Proof. Proof using. apply/setP => S; rewrite /porbits inE. apply/imsetP/orP => [[x _ ->{S}] | [] /imsetP[T /imsetP[x _] ->{T}] ->{S}]. - rewrite -(splitK x); case: splitP => j _ {x}. + left; apply/imsetP; exists (porbit s.1 j) => /=; first exact: imset_f. exact: porbit_tinj_lshift. + right; apply/imsetP; exists (porbit s.2 j) => /=; first exact: imset_f. exact: porbit_tinj_rshift. - by exists (lshift n x); last by rewrite porbit_tinj_lshift. - by exists (rshift m x); last by rewrite porbit_tinj_rshift. Qed.
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