proposition: Lemma porbit_tinj_rshift s a : porbit (tinj s) (rshift m a) = [set @rshift m n x | x in porbit s.2 a].
proof: Proof. Proof using. apply/setP => /= Y. apply/porbitP/imsetP => /= [[i ->]|[y]]. - exists ((s.2 ^+ i) a); first by apply /porbitP; exists i. exact: expg_tinj_rshift. - move /porbitP => [i ->] ->. by exists i; rewrite expg_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