proposition: Lemma psupport_card_porbit s x : (#|porbit s x| != 1%N) = (x \in psupport s).
proof: Proof. Proof using. rewrite inE; congr negb; apply/eqP/idP => [H|]. - by apply/afix1P => /=; rewrite -{2}(iter_porbit s x) H. - rewrite -afix_cycle_in; last by rewrite inE. by move/orbit1P; rewrite porbitE /= => ->; rewrite cards1. 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