cases h with
| inl h =>
simp only [min, if_pos (le_of_eq h)]
sorry
| inr h =>
simp only [add_comm a b, min, if_neg (not_le_of_lt h)]
apply le_of_eq
rw [nat_val_add_eq_min p b a h]
simp
exact h.le
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b ∨ nat_valuation p b < nat_valuation p a
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
no goals