rw [← factor_p_of_le_val evr (_ : n ≤ evr.valtn (x * y)), ← mul_assoc,
  ← factor_p_of_le_val evr hx]
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
⊢ p ^ n * sub_val evr n (x * y) = p ^ n * (sub_val evr n x * y)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ ↑n ≤ v evr.valtn (x * y)