induction n with
| zero => simp [sub_val_eq]
| succ n ih => simpa [sub_val_eq, decr_val_zero] using ih
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
n : ℕ
⊢ sub_val evr n 0 = 0
no goals