proposition: Lemma permCT_exists : {s | cycle_type s == ct}.
proof: Proof. Proof using. apply sigW => /=. have:= ex_set_setpart_shape (cast_intpartn (esym (cardsT T)) ct). move=> [P /perm_of_setpartE /= Hct Hshape]. exists (perm_of_setpart P); apply/eqP/val_inj => /=; rewrite Hct. by rewrite Hshape cast_intpartnE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(tuple finfun finset path bigop) mathcomp(fingroup perm action) mathcomp(ssralg matrix mxalgebra algC classfun) partition tools sorted permcomp fibered_set cycles