Arithmetic progression

Conjectura.Defs.Mathematics.Combinatorics.ArithmeticProgression

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Set.Defs
import Mathlib.Data.Nat.Notation

/-! # Arithmetic progression -/

namespace Conjectura.Combinatorics

/-- A set of naturals **contains an arithmetic progression of length `k`** when some `a` and
positive common difference `d` place all of `a, a+d, …, a+(k-1)d` inside it. -/
def ContainsAPOfLength (S : Set ℕ) (k : ℕ) : Prop :=
  ∃ a d : ℕ, 0 < d ∧ ∀ i < k, a + i * d ∈ S

end Conjectura.Combinatorics