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

State before:
A B : Set ℕ
n : ℕ
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
Tactic:
rw [schnirelmannDensity_le_one.ge_iff_eq, schnirelmannDensity_eq_one_iff]
State after:
no goals