proposition: Lemma porbit_restr_perm s x : porbit (restr_perm (porbit s x) s) x = porbit s x.
proof: Proof. Proof using. case: (boolP (porbit s x \in porbit_set s)) => [Hx|]. - have Hiter (i : nat) : (restr_perm (porbit s x) s ^+ i) x = (s^+i) x. elim: i => [|n Hn]; first by rewrite !expg0 !perm1. rewrite !expgSr !permM {}Hn (restr_permE (porbit_set_astabs _)) //. by rewrite -eq_porbit_mem porbit_perm eq_porbit_mem. apply/setP => z; apply/porbitP/porbitP => [] [n]. + by rewrite Hiter => ->; exists n. + by rewrite -Hiter => ->; exists n. - rewrite inE imset_f //= psupport_card_porbit in_psupport negbK => H. apply/eqP; have:= H; rewrite porbit_fix => /eqP ->; rewrite -porbit_fix. by rewrite restr_permE ?inE //=; apply/subsetP => y; rewrite !inE => /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