proposition: Lemma permCT_colpartn_card : permCT (colpartn #|T|) = 1%g.
proof: Proof. have /conj_permP[s ->] : cycle_type 1 == cycle_type (permCT (colpartn #|T|)). by rewrite permCTP cycle_type1. by rewrite conj1g. 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