proposition: Lemma conjG_is_action : is_action setT (@conjG_group gT).
proof: Proof. apply: is_total_action => [G | G x y]; apply: val_inj; rewrite /= ?act1 //. exact: actM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)