case mp =>
  intro (_ : n < m)
  show lt n m
  have : step n ≤ m := ‹n < m›
  have : step n ≤ step m := Nat.le_succ_of_le ‹step n ≤ m›
  have : n ≤ m := Nat.le_of_succ_le_succ ‹step n ≤ step m›
  have : le n m := prelude_le_iff_impl_le.mp ‹n ≤ m›
  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)›
  have : lt n m := And.intro ‹le n m› ‹n ≄ m›
  exact this
n m : Nat
⊢ n < m → lt n m
no goals