norm_cast
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
ih : v evr.valtn (sub_val evr n x) = ↑(Nat.succ m) - ↑n
⊢ ↑(Sub.sub ↑(Nat.succ m) ↑n) - 1 = ↑(Nat.succ m) - ↑(n + 1)
no goals