case zero =>
  intro (_ : Positive (0:ℕ))
  apply False.elim
  show False
  have : (0:ℕ) ≄ 0 := Signed.positive_defn.mp ‹Positive (0:ℕ)›
  apply this
  show 0 ≃ 0
  exact Rel.refl
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive 0 → ∃ m, step m ≃ 0
no goals