exact pow_ne_zero n (p_non_zero evr.valtn)
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n ≠ 0
no goals