proposition: Lemma faithful_isom (A : {group aT}) S (nSA : actby_cond A S to) : [faithful A, on S | to] -> isom A (actperm <[nSA]> @* A) (actperm <[nSA]>).
proof: Proof. by move=> ffulAS; apply/isomP; rewrite ker_actperm astab_actby setIT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)