exact Iff.mpr Nat.not_le (le_of_max_le_right hpm) (hmx p hpl)
case h.right.left.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
hpl : p ∈ l'
⊢ False
no goals