Erdős Problem 371

Reference: erdosproblems.com/371

theorem Erdos371.erdos_371 : {n : ℕ | (n + 1).maxPrimeFac > n.maxPrimeFac}.HasDensity (1 / 2)

Let $P(n)$ denote the largest prime factor of $n$. Show that the set of $n$ with $P(n+1) > P(n)$ has density $\frac{1}{2}$.