English
In Nat, the count of numbers in [0, b) congruent to v modulo r equals ceil((b − v mod r)/r).
Русский
В Nat число чисел в [0, b), эквивалентных v по модулю r, равно ceil((b − v mod r)/r).
LaTeX
$$$b.count( x \equiv v [MOD\ r] ) = \left\lceil \frac{b - (v \bmod r)}{r} \right\rceil$$
Lean4
/-- There are `⌈(b - v % r) / r⌉` numbers in `[0, b)` congruent to `v` mod `r`. -/
theorem count_modEq_card_eq_ceil (v : ℕ) : b.count (· ≡ v [MOD r]) = ⌈(b - (v % r : ℕ)) / (r : ℚ)⌉ :=
by
have hr' : 0 < (r : ℚ) := by positivity
rw [count_eq_card_filter_range, ← Ico_zero_eq_range, Ico_filter_modEq_card _ _ hr,
max_eq_left (sub_nonneg.mpr <| by gcongr; positivity)]
conv_lhs =>
rw [← div_add_mod v r, cast_add, cast_mul, add_comm]
tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne', Int.ceil_sub_natCast]
rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]
rw [sub_eq_self, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', neg_one_mul, zero_mul,
neg_lt_neg_iff, cast_lt]
exact ⟨mod_lt _ hr, by simp⟩
