proposition: Lemma restr_perm_neq X s x : restr_perm X s x != x -> restr_perm X s x = s x.
proof: Proof. Proof using. move=> Hx; rewrite restr_permE //; apply/contraR: Hx. - by move=> /triv_restr_perm ->; rewrite perm1. - by move/(out_perm (restr_perm_on X s)) ->. 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