by_contra! h
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
⊢ n ∈ A + B
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
⊢ False