proposition: Lemma in_porbit_setP s X x: reflect (exists2 X, X \in porbit_set s & x \in X) (s x != x).
proof: Proof. Proof using. rewrite -in_psupport; apply (iffP idP) => [Hy | [Y]]. - by exists (porbit s x); first by rewrite inE imset_f ?psupport_card_porbit. - rewrite inE => /andP[/imsetP[y _ -> {Y}] Hcard]. by rewrite -psupport_card_porbit -eq_porbit_mem => /eqP ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp