proposition: Lemma commVg : [~ x^-1, y] = [~ x, y]^-1.
proof: Proof. apply/eqP; rewrite commgEl eq_sym eq_invg_mul invgK mulgA -cxz. by rewrite -conjg_mulR -conjMg mulgV conj1g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)