proposition: Lemma permX_fix s x n : s x = x -> (s ^+ n) x = x.
proof: Proof. move=> Hs; elim: n => [|n IHn]; first by rewrite expg0 perm1. by rewrite expgS permM Hs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)