Counting terms of a natural-number arithmetic progression up to a deadline

Given a start d, step p, and deadline T, Cslib.arithmeticProgressionCount d p T counts the natural numbers t ≤ T of the form d + k * p (Cslib.arithmeticProgressionCount_spec), with p = 0 representing a singleton at d.

Main definitions

• Cslib.arithmeticProgressionCount: count of progression terms d + k * p in {0, …, T}.

Main results

• Cslib.arithmeticProgressionCount_spec: Set.ncard {t : ℕ | t ≤ T ∧ ∃ k, t = d + k * p} equals arithmeticProgressionCount d p T.

def Cslib.arithmeticProgressionCount (d p T : ℕ) : ℕ

Number of progression terms d + k * p in {0, ..., T}, with p = 0 denoting a singleton visit at d.

theorem Cslib.arithmeticProgressionCount_spec (d p T : ℕ) : {t : ℕ | t ≤ T ∧ ∃ (k : ℕ), t = d + k * p}.ncard = arithmeticProgressionCount d p T

arithmeticProgressionCount d p T counts the times t ≤ T of the form d + k * p.