norm_cast
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ ↑(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.range N)).card ≤ (Finset.filter Nat.Prime (Finset.range (N + 1))).card