proposition: Lemma perm_act1P a : reflect (forall x, aperm x a = x) (a == 1).
proof: Proof. apply: (iffP eqP) => [-> x | a1]; first exact: act1. by apply/permP=> x; rewrite -apermE a1 perm1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)