proposition: Lemma mact_is_action : is_action D mact.
proof: Proof. split=> [a x y | x a b Da Db]; first exact: perm_inj. by rewrite /mact morphM //= permM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)