English
For Nat b and modulus r, the number of x with x ≡ v (mod r) in [0,b) equals b/r plus 1 if v mod r < b mod r, and 0 otherwise.
Русский
Для b и модуля r число x с x ≡ v (mod r) в [0,b) равно b/r плюс 1, если v mod r < b mod r, иначе 0.
LaTeX
$$$b.count( x \equiv v [MOD\ r] ) = b / r + \begin{cases}1, & v \bmod r < b \bmod r \\ 0, & \text{иначе} \end{cases}$$$
Lean4
/-- There are `b / r + [v % r < b % r]` numbers in `[0, b)` congruent to `v` mod `r`,
where `[·]` is the Iverson bracket. -/
theorem count_modEq_card (v : ℕ) : b.count (· ≡ v [MOD r]) = b / r + if v % r < b % r then 1 else 0 :=
by
have hr' : 0 < (r : ℚ) := by positivity
rw [← ofNat_inj, count_modEq_card_eq_ceil _ hr, cast_add]
conv_lhs =>
rw [← div_add_mod b r, cast_add, cast_mul, ← add_sub, _root_.add_div, mul_div_cancel_left₀ _ hr'.ne', add_comm,
Int.ceil_add_natCast, add_comm]
rw [add_right_inj]
split_ifs with h
· rw [← cast_sub h.le, Int.ceil_eq_iff, div_le_iff₀ hr', lt_div_iff₀ hr', cast_one, Int.cast_one, sub_self, zero_mul,
cast_pos, tsub_pos_iff_lt, one_mul, cast_le, tsub_le_iff_right]
exact ⟨h, ((mod_lt _ hr).trans_le (by simp)).le⟩
· rw [cast_zero, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', zero_mul, tsub_nonpos, ←
neg_eq_neg_one_mul, neg_lt_sub_iff_lt_add, ← cast_add, cast_lt, cast_le]
exact ⟨(mod_lt _ hr).trans_le (by simp), not_lt.mp h⟩
