Andrica's conjecture

Reference: Wikipedia

theorem andrica_conjecture (n : ℕ) : √↑(Nat.nth Prime (n + 1)) - √↑(Nat.nth Prime n) < 1

The inequality $\sqrt{p_{n+1}}-\sqrt{p_n} < 1$ holds for all $n$, where $p_n$ is the nth prime number.