fact: Record ucycle_planar_plain_quasicubic : Prop := UcyclePlanarPlainQuasicubic { ucycle_planar_plain_quasicubic_base :> ucycle_plain_quasicubic; ucycle_planar_plain_quasicubic_is_planar :> planar G }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)