proposition: Lemma faithfulP A S : reflect (forall a, a \in A -> {in S, to^~ a =1 id} -> a = 1) [faithful A, on S | to].
proof: Proof. apply: (iffP subsetP) => [Cto1 a Aa Ca | Cto1 a]. by apply/set1P; rewrite Cto1 // inE Aa; apply/astabP. by case/setIP=> Aa /astabP Ca; apply/set1P; apply: Cto1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)