case step =>
  intro m
  show Positive (n + step m)
  apply AA.substFn (Rel.symm add_step)
  show Positive (step (n + m))
  apply Signed.positive_defn.mpr
  show step (n + m) ≄ 0
  exact step_neqv_zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)
no goals