proposition: Lemma commXg : [~ x ^+ i, y] = [~ x, y] ^+ i.
proof: Proof. elim: i => [|i' IHi]; first exact: comm1g. by rewrite !expgS commMgJ /conjg commuteX // mulKg IHi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)