exact absurd ‹Natural.step (0 : ℕ) ≃ 0› Natural.step_neqv_zero
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝¹ : coe 1 ≃ coe 0
this✝ : 1 ≃ 0
this : Natural.step 0 ≃ 0
⊢ False
no goals