. rw [max_of_lt ab]
  exact h.right
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 mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c