rw [← Nat.cast_le (α := ℝ), ← one_le_div (by positivity)]
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ n ≤ countelements A n + countelements B n
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑(countelements A n + countelements B n) / ↑n