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

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

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ sub_val evr Nat.zero 0 = 0
Tactic:
simp [sub_val_eq]
State after:
no goals

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
n : ℕ
ih : sub_val evr n 0 = 0
⊢ sub_val evr (Nat.succ n) 0 = 0
Tactic:
simpa [sub_val_eq, decr_val_zero] using ih
State after:
no goals