proposition: Lemma modact_faithful G S : [faithful G / 'C_G(S | to), on S | mod_action 'C_G(S | to)].
proof: Proof. rewrite /faithful astab_mod ?subsetIr //=. by rewrite -quotientIG ?subsetIr ?trivg_quotient. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)