proposition: Lemma porbit_set_restr s X : X \in porbit_set s -> porbit_set (restr_perm X s) = [set X].
proof: Proof. Proof using. move=> /[dup] H; rewrite inE => /andP[/imsetP[x _ Hx] HX]; subst X. apply/setP => Y; rewrite [RHS]inE. apply/idP/idP => [HY | /eqP->{Y}]. - have HYX : Y \subset (porbit s x). rewrite -(psupport_restr_perm H). rewrite -(cover_partition (partition_psupport _)). by apply (bigcup_max _ HY). rewrite eqEsubset; apply/andP; split => //. move: HYX => /subsetP HYX. move: HY; rewrite inE => /andP[/imsetP[y _ Hy] _]. have:= porbit_id (restr_perm (T:=T) (porbit s x) s) y. rewrite -Hy => /HYX; rewrite -eq_porbit_mem => /eqP Heq. by rewrite Hy -Heq porbit_restr_perm. - rewrite inE HX andbT. apply/imsetP; exists x => //. by apply esym; apply porbit_restr_perm. 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