Planar graphs are 9/2-colorable

We show that every planar graph $G$ has a 2-fold 9-coloring. In particular, this implies that $G$ has fractional chromatic number at most $\frac{9}{2}$. This is the first proof (independent of the 4 Color Theorem) that there exists a constant $k<5$ such that every planar $G$ has fractional chromatic number at most $k$.