Formal target: Corpus.Green72.NoKInLine

The **no-k-in-line problem**: For $N \geq k$ and $k > 2$, the AllowedSetSize is $(k - 1) N$, i.

Exact formal statement

∀ {k N : Nat}, LT.lt.{0} 2 k → LE.le.{0} k N → Corpus.Green72.NoKInLineFor k N

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

Environment availability: available.