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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
⊢ min (int_val p a) (int_val p b) ≤ int_val p (a + b)
Tactic:
simp [int_val, natAbs_add]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
⊢ nat_valuation p (natAbs a) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)) ∨
    nat_valuation p (natAbs b) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b))

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a b : ℤ
⊢ nat_valuation p (natAbs a) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)) ∨
    nat_valuation p (natAbs b) ≤ nat_valuation p (max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b))
Tactic:
sorry
State after:
no goals