have : n ≄ m := by
  intro (_ : n ≃ m)
  show False
  have : n = m := ‹n ≃ m›
  rw [‹n = m›] at ‹step n ≤ m›
  have : ¬(step m ≤ m) := Nat.not_succ_le_self m
  exact absurd ‹step m ≤ m› ‹¬(step m ≤ m)›
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ lt n m
n m : Nat
x✝ : n < m
this✝³ : step n ≤ m
this✝² : step n ≤ step m
this✝¹ : n ≤ m
this✝ : le n m
this : n ≄ m
⊢ lt n m