have : n ≃ m := ‹n = m›
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
this : n = m
⊢ n ≃ m
n m : Nat
h✝¹ : ¬n < m
h✝ : n = m
h : Ordering.eq = Ordering.eq
this✝ : n = m
this : n ≃ m
⊢ n ≃ m