constructor
case h.a.mpr
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
case h.a.mpr.left
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ d ∈ s.support

case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ (primorial ⌊z⌋₊).Coprime d