Theorem: SurjVal.val_neg (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x p : R
nav : SurjVal p
⊢ v nav (-x) = v nav x
Tactic:
rw [←one_mul x, neg_mul_eq_neg_mul, nav.v_mul_eq_add_v, val_of_minus_one, one_mul, zero_add]
State after:
no goals