refine induction_on_primes zero one ?_ _
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 n
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)