proposition: Lemma expg_tinj_lshift s a i : (tinj s ^+ i) (lshift n a) = lshift n ((s.1 ^+ i) a).
proof: Proof. Proof using. elim: i => [|i IHi]; first by rewrite !expg0 !perm1. rewrite !expgSr !permM IHi permE /tinjval /=. pose y := inl ((s.1 ^+ i) a). by rewrite (_: lshift _ _ = unsplit (y _)) // unsplitK. 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