obtain rfl | hn := eq_or_ne n 0
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
⊢ n ≤ countelements A n + countelements B n
case inl
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ≤ countelements A 0 + countelements B 0

case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ n ≤ countelements A n + countelements B n