cases Nat.eq_or_lt_of_le h <;> (clear h ; rename_i h)
case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a
case inr.inl
a b : Nat
h : b = a
⊢ Nat.max a b = Nat.max b a

case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a