repeat rw [countelements]
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ countelements A (n - 1) = countelements A n
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card = (filter (fun x => x ∈ A) (Icc 1 n)).card