Erdős Problem 488

Reference: erdosproblems.com/488

theorem erdos_488 : (∀ (A : Finset ℕ) (n m : ℕ), m > n → A.max ≤ ↑n → ↑(Finset.filter (fun (x : ℕ) => x ∈ {n : ℕ | n ≥ 1 ∧ ∀ a ∈ A, ¬a ∣ n}) (Finset.Icc 1 m)).card / ↑m < 2 * ↑(Finset.filter (fun (x : ℕ) => x ∈ {n : ℕ | n ≥ 1 ∧ ∀ a ∈ A, ¬a ∣ n}) (Finset.Icc 1 n)).card / ↑n) ↔ False

Let $A$ be a finite set and $$B = \{n \ge 1 : a \nmid n \text{ for all } a \in A\}.$$ Is it true that, for every $m > n \ge \max(A)$, $$\frac{|B \cap [1, m]|}{m} < 2 \frac{|B \cap [1, n]|}{n}?$$