Theorem: Int.int_val_add_eq_min (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
h : int_val p a < int_val p b
⊢ int_val p (a + b) = int_val p a
Tactic:
sorry
State after:
no goals