proposition: Lemma cface_node_ecpK : cface (node ecpK) (icpK (node x0)).
proof: Proof. rewrite /ecpK ecpR1_eq edgeK ecpR'_eq; apply: cface_ecpN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)