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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
⊢ sub_val evr (Nat.succ m) x = sub_val evr m (decr_val evr x)
Tactic:
simp [sub_val_eq]
State after:
no goals