proposition: Lemma injm_faithful : 'injm phi -> [faithful D, on setT | morph_action].
proof: Proof. move/injmP=> phi_inj; apply/subsetP=> a /setIP[Da /astab_act a1]. apply/set1P/phi_inj => //; apply/permP=> x. by rewrite morph1 perm1 -mactE a1 ?inE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)