proposition: Lemma tinjA (s : 'S_m) (t : 'S_n) (u : 'S_p) : tinj (tinj(s, t), u) = cast_perm (addnA m n p) (tinj (s, tinj (t, u))).
proof: Proof. Proof using. apply/permP => /= itmp. rewrite -(splitK itmp) !permE. case: splitP => i _ {itmp}; rewrite /tinjval !unsplitK /= cast_permE. - rewrite -(splitK i) !permE. case: splitP => j _ {i}; rewrite /tinjval !unsplitK /=. + rewrite [cast_ord (esym _) _](_ : _ = unsplit (inl j)); last exact: val_inj. by rewrite !unsplitK /=; apply val_inj. + rewrite [cast_ord (esym _) _](_ : _ = unsplit (inr (lshift _ j))); last exact: val_inj. rewrite !unsplitK /=; apply val_inj => /=. rewrite (_: lshift _ _ = unsplit (inl j)) //. by rewrite !permE /tinjval !unsplitK /=. - rewrite [cast_ord (esym _) _](_ : _ = unsplit (inr (rshift _ i))); last by apply: val_inj => /=; rewrite addnA. rewrite !permE /tinjval !unsplitK /=. rewrite (_: rshift n _ = unsplit (inr i)) //. rewrite !permE /tinjval !unsplitK /=. by apply val_inj; rewrite /= addnA. 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