proposition: Lemma cpmap_planar cp : cubic_prog cp -> planar (cpmap cp).
proof: Proof. elim: cp => [_|s cp IHcp]. have geoG: ucycle_plain_quasicubic_connected (rev (@cpring cpmap0 true)). split; [split; last by rewrite cpring0 | exact: (@cpmap_connected [::])]. by split; [ apply: (@cpmap_plain [::]) | apply: (@cpmap_cubic [::])]. by rewrite (quasicubic_Euler geoG) cpring0 fcard_id card_bool. case: s => //= cp_ok; have [plainG cubicG] := (cpmap_plain cp_ok, cpmap_cubic cp_ok); have [ccG planarG] := (cpmap_connected cp_ok, IHcp cp_ok). - exact: planar_ecpY. - exact: planar_ecpH. exact: planar_ecpU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)