apply cases_on (motive := λ n => Positive n → ∃ m, step m ≃ n) n
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive n → ∃ m, step m ≃ n
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive 0 → ∃ m, step m ≃ 0

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ ∀ (m : ℕ), Positive (step m) → ∃ m_1, step m_1 ≃ step m