English
There are ⌈(b − v) / r⌉ − ⌈(a − v) / r⌉ numbers in Ico a b that are congruent to v modulo r, i.e., the Nat version mirrors the integer version.
Русский
В интервале Ico a b ровно ⌈(b − v) / r⌉ − ⌈(a − v) / r⌉ чисел, эквивалентных v по модулю r.
LaTeX
$$$\#\{x \in \mathrm{Ico}\ a\ b \mid x \equiv v \,[MOD\ r]\} = \max\left( \left\lceil \frac{b - v}{r} \right\rceil - \left\lceil \frac{a - v}{r} \right\rceil, 0 \right)$$
Lean4
/-- There are `⌈(b - v) / r⌉ - ⌈(a - v) / r⌉` numbers congruent to `v` mod `r` in `[a, b)`,
if `a ≤ b`. `Nat` version of `Int.Ico_filter_modEq_card`. -/
theorem Ico_filter_modEq_card (v : ℕ) :
#({x ∈ Ico a b | x ≡ v [MOD r]}) = max (⌈(b - v) / (r : ℚ)⌉ - ⌈(a - v) / (r : ℚ)⌉) 0 := by
simp_rw [← Ico_filter_modEq_cast _ _ ▸ card_map _, Int.Ico_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]
