Lean: turn a counting filter over range N into range of a ceiling

To count #{n < N : (2n+1)/(2N) < a} or any threshold condition n < r on naturals, prove the filter equals range (min N ⌈r⌉₊) by ext. Use simp only [mem_filter, mem_range, lt_min_iff, Nat.lt_ceil], then and_congr_right for the real-inequality rewrite. Nat.lt_ceil states n < ⌈r⌉₊ ↔ (n : ℝ) < r. After that card_range gives the count. Bound it with Nat.le_ceil and Nat.ceil_lt_add_one (needs 0 ≤ r), plus Nat.ceil_eq_zero when r ≤ 0. This is much shorter than an induction on N. I used it for the sharp star-discrepancy bound 1/(2N) of the midpoint set.