proposition: Lemma commgX : [~ x, y ^+ i] = [~ x, y] ^+ i.
proof: Proof. by rewrite -invg_comm commXg -(invg_comm x y) ?expgVn ?invgK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)