Planar graphs with a Hamiltonian loop connecting all faces do not necessarily have a Hamiltonian on their edges, which would make a 3 edge coloring and thus a 4 face coloring easy. However they have a lot of great structure. If you split the graph along the face Hamiltonian using it like an equator,the edges in the northern or southern hemisphere form trees. Thus the problem of coloring Hamiltonian planar graphs with n faces reduces to finding a mutual edge 3 coloring of any two n trees.

Regarding the Hamiltonian graphs as compositions of trees makes them easily counted, and gives a relation between graphs by relating their trees.

Between trees of the same size: Any tree of size n may converted into another of size n by iterated diamond switches, DS, of internal branches. I have proven any n-tree can be converted into any other n-tree in less than 2n DS. Nicely, if 2 trees are within n DS they have a mutual coloring.

Between trees of different sizes: Larger and smaller Hamiltonian graphs can be made by adding or subtracting branches that cross the equator, preserving the Hamiltonian loop. So inductive proofs are encouraged.

Also any tree of n roots has exactly 2^(n-3) colorings , which can be arranged on a hypercube, so you could prove all Hamiltonian graphs with n faces are colorable by proving any two color-hypercubes of n-trees intersect.

Hamiltonian graphs are a good restricted simpler group of graphs to try to prove colorable, interesting in their own right. They are even more important if their colorability implies the colorability of all planar graphs. Is it so?