obtain ⟨l', hl', hlnd, hlp⟩ := ih
case succ
m n : ℕ
ih : ∃ lst, lst.length = n ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
case succ.intro.intro.intro
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x