Theorem: countelements_nonneg (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

State before:
A✝ B : Set ℕ
n✝ : ℕ
A : Set ℕ
n : ℕ
⊢ 0 ≤ countelements A n
Tactic:
positivity
State after:
no goals