Ben Green's Open Problem 7

References:

• [Ben Green's Open Problem 81](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.1 Problem 7)
• erdosproblems.com/341

theorem Green7.green_7.variants.queneau : sorry ↔ ∀ (a : ℕ → ℤ), (∀ᶠ (n : ℕ) in Filter.atTop, IsLeast {x : ℤ | a n < x ∧ x ∉ {x : ℤ | ∃ i ≤ n, ∃ j ≤ n, a i + a j = x}} (a (n + 1))) → have d := fun (i : ℕ) => a (i + 1) - a i; ∃ p > 0, ∀ᶠ (m : ℕ) in Filter.atTop, d (m + p) = d m