. rw [max_of_ge ab] at h
  exact ⟨h, trans ab h⟩
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 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