exact ⟨_, hxA, x, hxB, tsub_add_cancel_of_le hx.1.le⟩
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : x < n ∧ n - x < n
⊢ n ∈ A + B
no goals