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

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