rw [sub_le_iff_le_add, add_comm_sub]
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
γ : ℝ := schnirelmannDensity (A + B)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 - γ ≤ 1 - (α + β - α * β)
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
γ : ℝ := schnirelmannDensity (A + B)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 ≤ 1 + (γ - (α + β - α * β))