Theorem: ENatValRing.sub_val_mul_right (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hy : ↑n ≤ v evr.valtn y
⊢ sub_val evr n (x * y) = x * sub_val evr n y
Tactic:
rw [mul_comm x y, sub_val_mul_left evr hy, mul_comm]
State after:
no goals