proposition: Lemma conjg_is_groupAction : is_groupAction setT conjg_action.
proof: Proof. move=> a _; rewrite inE; apply/andP; split; first by apply/subsetP=> x /[1!inE]. by apply/morphicP=> x y _ _; rewrite !actpermE /= conjMg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)