proposition: Lemma commgXVg x n : [~ x, x ^- n] = 1.
proof: Proof. exact/eqP/commgP/commuteV/commuteX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)