proposition: Lemma card_psupport_conjg s a : #|psupport s| = #|psupport (s ^ a)%g|.
proof: Proof. Proof using. rewrite psupport_conjg. apply esym; apply card_imset. exact: perm_inj. 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