proposition: Lemma perm_faithful A : [faithful A, on setT | perm_action].
proof: Proof. apply/subsetP=> a /setIP[Da crTa]. by apply/set1P; apply/permP=> x; rewrite -apermE perm1 (astabP crTa) ?inE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)