In Edsger Dijkstra's monograph "Notes on Structured Programming", he describes a simple imperative program for generating an array of the first $n$ primes. For each prime $p_n$, it finds the next prime by checking each odd $j \gt p_n$, to see if it has a prime divisor $d$ in the range $2 \lt d \le \sqrt j$. The algorithm draws these candidates from the array of prime numbers it has been constructing, which at any given iteration contains the primes between $2$ and $p_n$ inclusive, so there is an implicit assumption is that $\sqrt j \le p_n$ (the algorithm iterates over the array of primes up to $p_n$ with the only termination conditions being $d|j$ or $d > \sqrt j$, so if $\sqrt j$ could be $\ge p_n$ we risk reading past the end of the array). Quoting Dijkstra:
In all humility I quote Don Knuth's comment on an earlier version of this program, where I took this fact for granted:
"Here you are guilty of a serious omission! Your program makes use of a deep result of number theory, namely that if $p_n$ denotes the $n$th prime number we always have $p_{n+1} < p_n^2$."
So I'm curious about the history of this "deep result", and how difficult the proof is.