constructor
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ↔ p ≤ n
case mp
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p → p ≤ n

case mpr
n p : ℕ
hp : p.Prime
⊢ p ≤ n → p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p