proposition: Lemma cycle_type_tinj s : ct (tinj s) = ct s.1 +|+ ct s.2.
proof: Proof. Proof using. apply val_inj; rewrite union_intpartnE cast_intpartnE /=. rewrite porbits_tinj setpart_shape_union; first last. rewrite -setI_eq0; apply/eqP/setP => S. rewrite !inE; apply/negP => /andP[]. move=> /imsetP[X /imsetP[x _ ->]] -> {X}. move=> /imsetP[X /imsetP[y _ ->]]. move/setP => /(_ (lshift n x)). rewrite imset_f; last exact: porbit_id. move=> /esym/imsetP => [] [z _] /eqP. by rewrite eq_lrshift. by congr sort; rewrite /ct !cast_intpartnE /=; congr (_ ++ _); apply setpart_shape_imset; [exact: lshift_inj | exact: rshift_inj]. 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