apply cases_on (motive := λ m => Positive (n + m)) m
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + m)
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)