Formal target: Corpus.OEIS67720.prime_add_one_of_a

For members of the sequence other than $8$, we have $k + 1$ is prime.

Exact formal statement

∀ {k : Nat}, Corpus.OEIS67720.A k → Ne.{1} k 8 → Nat.Prime (HAdd.hAdd.{0, 0, 0} k 1)

This target is a formal statement, not a proof of the problem.

Environment availability: available.