constructor <;> intro h
<;> (cases Nat.lt_or_ge a b) <;> rename_i ab
a b c : Nat
⊢ Nat.max a b ≤ c ↔ a ≤ c ∧ b ≤ c
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