induction n using Nat.caseStrongInductionOn with
| zero => exact zero
| ind k h_ind =>
  cases dec_em (Nat.Prime k.succ) with
  | inr hk_prime =>
    apply not_prime _ hk_prime
    exact h_ind
  | inl hk_prime =>
    cases Nat.Prime.eq_two_or_odd' hk_prime with
    | inl hk_two => rw [hk_two]; exact two
    | inr hk_two =>
      cases hk_two with
      | intro m hm =>
        simp [Nat.add_one] at hm
        simp [hm] at *
        apply odd_prime _ hk_prime h_ind
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
n : ℕ
⊢ p n
no goals