cases lt_trichotomy (nat_valuation p a) (nat_valuation p b) with | inl h =>
  simp only [min, if_pos (le_of_lt h)]
  apply le_of_eq
  rw [nat_val_add_eq_min p a b h]
  rw [inf_eq_left]
  exact h.le
| inr h => 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
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
no goals