case step =>
  intro k (ih : m ≤ k → n ≤ k) (_ : m ≤ step k)
  show n ≤ step k
  match le_step_split ‹m ≤ step k› with
  | Or.inl (_ : m ≤ k) =>
    exact le_step (ih ‹m ≤ k›)
  | Or.inr (_ : m ≃ step k) =>
    exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1
no goals