proposition: Lemma restr_perm_commute s : commute (restr_perm s) s.
proof: Proof. have [sC|/triv_restr_perm->] := boolP (s \in 'N(S | 'P)); last first. exact: (commute_sym (commute1 _)). apply/permP => x; have /= xsS := astabsP sC x; rewrite !permM. have [xS|xNS] := boolP (x \in S); first by rewrite ?(restr_permE) ?xsS. by rewrite !(out_perm (restr_perm_on _)) ?xsS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)