Planar graphs are surprisingly difficult to formalize. The textbook definition (can be drawn on a plane) is easy to understand, but in code that explodes into a mess of coordinate geometry.

Georges Gonthier, in his proof of the four-color theorem, used a structure called combinatorial hypermaps to encode planar graphs. This approach seems most promising. Before proposing that to mathlib, it would be nice to check that it's suitable for all planar graph theorems, not just four-color.

Resolves YES if mathlib has a definition of planar graph. The code must be on the master branch. Alternative definitions of graphs (like hypermaps) are allowed, as long as there is an embedding from SimpleGraph that preserves planarity.