no goals
R : Type u_2
inst✝³ : CommRing R
x : R
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZpow x B (-d) * selfZpow x B d = 1
rw [mul_comm, selfZpow_mul_neg x B d]