exact Set.InjOn.mono (fun x hx ↦ (mem_Ioo.1 (mem_filter.1 hx).1).2.le) $
  fun x hx y hy ↦ tsub_inj_right hx hy
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))
no goals