induction n with
| zero => simp [sub_val_x_zero]
| succ n ih =>
  cases @eq_zero_or_pos _ _ (evr.valtn x) with
  | inl h' =>
    have h'm : evr.valtn (-x) = 0 := by simp [h']
    rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
  | inr h' =>
    rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
    decr_val_neg, sub_val_decr_val_comm]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ sub_val evr n (-x) = -sub_val evr n x
no goals