rintro p (_ | _ | a) hp ha
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ ∀ (p a : ℕ), p.Prime → P a → P (p * a)
case zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P 0
⊢ P (p * 0)

case succ.zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P (0 + 1)
⊢ P (p * (0 + 1))

case succ.succ
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p a : ℕ
hp : p.Prime
ha : P (a + 1 + 1)
⊢ P (p * (a + 1 + 1))