Reading the Wikipedia page about the well-know Nine dots puzzle, I have just seen that the planar generalization of this problem would have been proven in 1956 (see Wikipedia: Nine dots puzzle), while my thought was that the problem has remained unsolved for many decades, until 2013, when Balázs Keszegh released its "Covering Paths and Trees for Planar Grids" (see https://arxiv.org/abs/1311.0452).
Now, I like very much the aforementioned proof, strict and clean (moreover, some years ago, I tried to independently prove the same statement since I was unaware of other proofs... then I found that there already was valid proof and I gladly avoided to write a proper paper restating the same).
Thus, my question is as follows:
Let $n$ be an integer greater than $4$. Which is the first published, formally correct (i.e., valid from a mathematical point of view), proof that every optimal polygonal chain that visits any given $\{0,1,\ldots,n-1\} \times \{0,1,\ldots,n-1\}$ grid of $n^2$ points in $\mathbb{R}^2$ has (exactly) $2 \cdot n-2$ edges and then, which is the first known proof that showed the same result for the minimum number of edges charaterizing an optimal covering circuit for the same set of points?
