case zero =>
  show Positive (n + 0)
  apply AA.substFn (Rel.symm add_zero)
  exact ‹Positive n›
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)
no goals