proposition: Lemma cpmap_connected cp : cubic_prog cp -> connected (cpmap cp).
proof: Proof. elim: cp => [_ | s cp IHcp]. apply/eqP/esym; rewrite -(n_comp_connect (@glinkC cpmap0) true). by apply: eq_n_comp_r => [] []; rewrite ?inE connect1. case: s => // /IHcp ccG. - exact: connected_ecpY. - exact: connected_ecpH. exact: connected_ecpU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)