cases m with
| zero =>
  simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
    ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
  rw [sub_val_val_zero evr x n.succ h]
  exact h
| succ m =>
  rw [sub_val_val_pos_succ, sub_val_decr_val_comm, val_decr_val evr (sub_val evr n x) ih,
    Nat.succ_eq_add_one n]
  norm_cast
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑m
n : ℕ
ih : v evr.valtn (sub_val evr n x) = ↑m - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑m - ↑(Nat.succ n)
no goals