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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = 0
⊢ sub_val evr m x = x
Tactic:
induction m with
| zero => exact sub_val_x_zero evr x
| succ m ih => simpa [sub_val_eq, zero_valtn_decr _ h] using ih
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
⊢ sub_val evr Nat.zero x = x
Tactic:
exact sub_val_x_zero evr x
State after:
no goals

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