calc
  _ ≤ _ := hAB
  _ ≤ _ := add_le_add (schnirelmannDensity_le_div hn) (schnirelmannDensity_le_div hn)
  _ = _ := by push_cast; rw [add_div]; rfl
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
no goals