. rw [max_of_eq h, max_of_eq' h.symm]
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
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a