congr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ (filter (fun x => x ∈ B) (Ioo 0 n)).card = (filter (fun x => x ∈ B) (Icc 1 (n - 1))).card

A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))
case e_s.e_s.e_b
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ n = ((n - 1).add 0).succ

A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))