rw [nat_val_add_eq_min p a b h]
case inl.a
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)
case inl.a
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