. rw [max_of_lt ab] at h
  exact ⟨Nat.le_of_lt (trans ab h), h⟩
case mp.inl
a b c : Nat
h : Nat.max a b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c

case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c