English
There are exactly ⌊n/p⌋ natural numbers in the interval (0, n] that are divisible by p.
Русский
В промежутке (0, n] ровно ⌊n/p⌋ чисел делятся на p.
LaTeX
$$$ \#\{ x \in (0, n] \mid p \mid x \} = \left\lfloor\dfrac{n}{p}\right\rfloor $$$
Lean4
/-- Exactly `n / p` naturals in `(0, n]` are multiples of `p`. -/
theorem Ioc_filter_dvd_card_eq_div (n p : ℕ) : #({x ∈ Ioc 0 n | p ∣ x}) = n / p := by
induction n with
| zero => simp
| succ n IH =>
-- TODO: Golf away `h1` after Yaël PRs a lemma asserting this
have h1 : Ioc 0 n.succ = insert n.succ (Ioc 0 n) :=
by
rcases n.eq_zero_or_pos with (rfl | hn)
· simp
simp_rw [← Ico_add_one_add_one_eq_Ioc, Ico_insert_right (add_le_add_right hn.le 1), Ico_add_one_right_eq_Icc]
simp [Nat.succ_div, add_ite, add_zero, h1, filter_insert, apply_ite card, IH, Finset.mem_filter, mem_Ioc,
not_le.2 (lt_add_one n)]
