The original proof appealed to minimality of $G_0$ to 4-color
$G_0/uv$, but $G_0/uv$ is not in general a triangulation, so it is
not directly covered by the minimality hypothesis (which is over
maximal planar graphs). Triangulate $G_0/uv$ into a maximal planar
$T$ on the same vertex set: $|V(T)| < |V(G_0)|$, so minimality gives
$T$ a 4-coloring, which restricts to $G_0/uv$.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
didericis
31dd217863