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) = mk' B 1 (Submonoid.pow x d)
simp [selfZpow_of_nonpos _ _ (neg_nonpos.mpr (Int.coe_nat_nonneg d))]