constructor
case h.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').Nodup ∧ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x
case h.right.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').Nodup

case h.right.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x