proposition: Theorem card_class_of_part n (l : 'P_n) : #|classCT l| = n`! %/ zcard l.
proof: Proof. Proof using. rewrite /classCT card_class_perm permCTP /=. by rewrite cast_intpartnE /= card_ord. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype