simp only [min, if_pos (le_of_eq h)]
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)