proposition: Lemma restr_perm_psupportE X s : restr_perm (psupport (restr_perm X s)) s = restr_perm X s.
proof: Proof. Proof using. case: (boolP (s \in 'N(X | 'P))) => [Hs|]; first last. move/triv_restr_perm ->; rewrite psupport1; apply/permP => x. by rewrite perm1 (out_perm (restr_perm_on _ _)) ?inE. apply/permP => x. case: (restr_perm X s x =P x) => [/[dup]{-1}-> /eqP | /eqP Hx]. - rewrite -[_ == _]negbK -in_psupport => /out_perm -> //. exact: restr_perm_on. - rewrite (restr_perm_neq Hx). move: Hx; rewrite -in_psupport => Hxsupp. rewrite restr_permE //. apply/astabsP => y /=; rewrite apermE. case: (boolP (y \in psupport (restr_perm X s))). + rewrite !in_psupport => /[dup]/restr_perm_neq Hy2. apply contra => /eqP; rewrite -{2}Hy2 => /perm_inj. by rewrite Hy2 => ->. + apply: contraNF => Hsy. suff: forall i, ((restr_perm (T:=T) X s ^+ i) (s y) = (s ^+ i.+1) y) /\ (s ^+ i.+1) y \in psupport (restr_perm (T:=T) X s). move=> /(_ #[s].-1) [_]. rewrite prednK; last exact: order_gt0. by rewrite expg_order perm1. elim=> [|i [IHi1 IHi2]]; first by rewrite expg0 expg1 perm1. have:= IHi2; rewrite in_psupport => /restr_perm_neq. rewrite -[RHS]permM -expgSr => <-. split; last by rewrite -psupport_stable. by rewrite !expgSr !permM IHi1 expgSr permM. 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