proposition: Lemma psupport_conjg s a : psupport (s ^ a) = [set a x | x in psupport s].
proof: Proof. Proof using. rewrite -!(cover_partition (partition_psupport _)) /porbit_set. rewrite porbits_conjg /cover (big_morph _ (imsetU _) (imset0 _)). rewrite -[RHS](big_imset id) /=; first last. by move=> X Y _ _; apply: imset_inj; apply perm_inj. apply/eq_bigl => X; rewrite !inE. apply/andP/imsetP => [[/imsetP[/= C HC ->{X}]] | [/= C]]. - rewrite card_imset; last exact: perm_inj. by move=> cardC; exists C; rewrite // inE HC cardC. - rewrite inE => /andP[HC cardC] ->{X}; split; first exact: imset_f. by rewrite card_imset; last 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