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