proposition: Lemma imset_classCT : [set classCT p | p in setT] = classes [set: {perm T}].
proof: Proof. Proof using. rewrite -setP => C. apply/imsetP/imsetP => [] [/= p _ Hp]. - by exists (permCT p); rewrite // inE. - exists (cycle_type p) => //. by rewrite Hp; apply /class_eqP; rewrite -classCTP. 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