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