split
n m : Nat
x✝ : n ≃ m
⊢ (if n < m then Ordering.lt else if n = m then Ordering.eq else Ordering.gt) = Ordering.eq
case isTrue
n m : Nat
x✝ : n ≃ m
h✝ : n < m
⊢ False

case isFalse
n m : Nat
x✝ : n ≃ m
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.eq