theorem int {A : Finset ℕ} {N : ℕ} (hAN : A ⊆ Finset.range N) (hA : ThreeAPFree ↑A) : ∃ c > 0, ↑A.card ≤ ↑N / Real.exp (-c * Real.log ↑N ^ 12⁻¹)