proposition: Lemma porbit_fix s x : (s x == x) = (porbit s x == [set x]).
proof: Proof. Proof using. rewrite -[LHS]negbK -in_psupport -psupport_card_porbit negbK. apply/eqP/eqP => [|->]; last by rewrite cards1. by rewrite !porbitE; move/card_orbit1. 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