apply nzero_mul_left_cancel (p ^ (n + m)) _ _ (pow_ne_zero _ (p_non_zero evr.valtn))
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ sub_val evr n x * sub_val evr m y = sub_val evr (n + m) (x * y)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ p ^ (n + m) * (sub_val evr n x * sub_val evr m y) = p ^ (n + m) * sub_val evr (n + m) (x * y)