proposition: Lemma card_pred_card_porbits s (P : pred nat) : #|[set x in porbits s | P #|x| ]| = count P (cycle_type s).
proof: Proof. Proof using. rewrite /cycle_type /= /porbit_set /setpart_shape. have /permPl/seq.permP -> := perm_sort geq [seq #{x} | x in porbits s]. rewrite cardE /enum_mem size_filter /= count_map count_filter. by apply eq_count => X; rewrite !inE andbC. 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