proposition: Lemma cycle_type_tinjC (s : 'S_m) (t : 'S_n) : cycle_typeSn (tinj (s, t)) = cycle_typeSn (cast_perm (esym (addnC m n)) (tinj (t, s))).
proof: Proof. rewrite !cast_cycle_typeSN !cycle_type_tinj /=. apply val_inj; rewrite [RHS]cast_intpartnE !union_intpartnE /=. apply/perm_sortP => //. by rewrite perm_catC. 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