obtain ⟨n, rfl⟩ := ha
G : Type u_1
inst✝ : Group G
g a b : G
ha : ∃ n, g ^ n = a
hb : ∃ n, g ^ n = b
⊢ a * b = b * a
case intro
G : Type u_1
inst✝ : Group G
g b : G
hb : ∃ n, g ^ n = b
n : ℤ
⊢ g ^ n * b = b * g ^ n