proposition: Lemma aperm_is_action : is_action setT (@aperm rT).
proof: Proof. by apply: is_total_action => [x|x a b]; rewrite apermE (perm1, permM). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)