proposition: Lemma injm_actm a : 'injm (actm to a).
proof: Proof. apply/injmP=> x y Rx Ry; rewrite /= /actm; case: ifP => Da //. exact: act_inj. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)