simp only [Finset.mem_filter, Finset.mem_range, and_imp]
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter Nat.Prime (Finset.range N) → n ∈ Finset.filter Nat.Prime (Finset.range (N + 1))
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → n.Prime → n < N + 1 ∧ n.Prime