congr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A (n - 1) + countelements B (n - 1)
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)
hun : (filter (fun x => x ∈ A) (Ioo 0 n) ∪ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
⊢ (filter (fun x => x ∈ A) (Ioo 0 n)).card + (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card =
    (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card + (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
case e_a.e_s.e_s.e_b
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A (n - 1) + countelements B (n - 1)
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)
hun : (filter (fun x => x ∈ A) (Ioo 0 n) ∪ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
⊢ n = ((n - 1).add 0).succ