Counting divisible by p

Stream: Is there code for X?

[Stuart Presnell]

Does mathlib already know that Ioc 0 n contains exactly n/p elements divisible by p?

example (n : ℕ) {p : ℕ} (hp : p ≠ 0) :
  ((Ioc 0 n).filter (λ x, p ∣ x)).card = n / p := sorry

[Patrick Johnson]

(hp : p ≠ 0) is redundant.

[Ruben Van de Velde]

docs#card_multiples is close