case isFalse =>
  split at h
  case isTrue =>
    have : n = m := by assumption
    have : n ≃ m := ‹n = m›
    exact this
  case isFalse =>
    have : n ≠ m := by assumption
    contradiction
n m : Nat
h✝ : ¬n < m
h : (if n = m then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ n ≃ m
no goals