rw [← h, sub_val_mul_sub_val _ _ _ hx hy]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m nm : ℕ
h : n + m = nm
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ sub_val evr nm (x * y) = sub_val evr n x * sub_val evr m y
no goals