proposition: Lemma tinjE1 (t : 'S_n) : tinj (t, 1%g) = cast_perm (esym (addn0 n)) t.
proof: Proof. apply/permP => /= itmp. rewrite -(splitK itmp) !permE. case: splitP => i _ {itmp}; last by case: i. by rewrite /tinjval !unsplitK /= -!cast_lshift cast_ord_permE. 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