. rw [max_of_lt h, max_of_gt h]
case inl
a b : Nat
h : a < b
⊢ Nat.max a b = Nat.max b a

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