simp [primes]
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ primes (Finset.range (Nat.succ (Nat.succ n))) = primes (Finset.range (Nat.succ n))
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (Finset.range (Nat.succ (Nat.succ n))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))