. rw [SurjVal.v_mul_eq_add_v]
  exact add_le_add hx hy
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
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
no goals