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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ sub_val evr n (x - y) = sub_val evr n x - sub_val evr n y
Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, sub_val_add evr hx, sub_val_neg]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn (-y)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn (-y)
Tactic:
simpa
State after:
no goals