proposition: Lemma adj_icpK : let adjx0 x y := cface (edge x0) x && cface (node x0) y in forall x y, adj (icpK x) (icpK y) = [|| adj x y, adjx0 x y | adjx0 y x].
proof: Proof. by move=> /= x y; apply: (etrans (adj_icpN ecpR' _ _)); rewrite ecpR'_eq nodeK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)