show m < step n
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ step n > m
case c
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n✝ m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
n : ℕ
ih : AA.OneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ m < step n