Erdős Problem 348

Reference: erdosproblems.com/348

theorem Erdos348.erdos_348 : {x : ℕ × ℕ | ∃ (m : ℕ) (n : ℕ) (_ : m < n) (a : ℕ → ℕ) (_ : Monotone a) (_ : ∀ (s : Finset ℕ), s.card = m → IsAddCompleteNatSeq (Function.updateFinset a s 0)) (_ : ∀ (t : Finset ℕ), t.card = n → ¬IsAddCompleteNatSeq (Function.updateFinset a t 0)), (m, n) = x} = sorry

For what values of $0 \leq m < n$ is there a complete sequence $A = \{a_1 \leq a_2 \leq \cdots\}$ of integers such that

1. $A$ remains complete after removing any $m$ elements, but
2. $A$ is not complete after removing any $n$ elements.