induction n with
| zero =>
  simpa [sub_val_x_zero]
| succ n ih =>
  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
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
h : v evr.valtn x = ↑m
⊢ v evr.valtn (sub_val evr n x) = ↑m - ↑n
no goals