proposition: Lemma embeddable_cfquiz : embeddable (cfring cf).
proof: Proof. split; try exact: cpradius2P; last first. by apply/allP=> x; rewrite mem_rev => r_x; case: cfquizP => /(_ x r_x). have cpQ := config_prog_cubic cp_ok; do !split. - exact: cpmap_plain. - exact: cpmap_cubic. - exact: ucycle_rev_cpring. - exact: cpmap_connected. - by move: (cpmap_simple cp_ok); rewrite simple_cat -simple_rev => /and3P[]. - exact: cpmap_planar. exact: cpmap_bridgeless. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)