rw [primesBetween]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ primesBetween 1 ↑n = (Finset.filter Nat.Prime (Finset.range (n + 1))).card
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊)).card = (Finset.filter Nat.Prime (Finset.range (n + 1))).card