theorem int : ∃ c > 0, ∃ C > 0, ∀ ⦃A : Finset ℕ⦄ ⦃N : ℕ⦄, A ⊆ Finset.range N → ThreeAPFree ↑A → ↑A.card ≤ ↑N / Real.exp (c * Real.log ↑N ^ 12⁻¹)