proposition: Lemma adj_ecpH u : adj ecpH u = (u \in fband (map icpH [:: node x0; x0; face (edge x0)])).
proof: Proof. rewrite adjF1 -[_ _ u]/(adj (icpN ecpY ecpY) u). have [v uFv] := fband_icpN u; rewrite (adjFr uFv) adj_icpN connect0 andbT. rewrite cfaceC !cface_ecpY (closed_connect (fbandF _) uFv) {u uFv}adj_ecpY. have <-: icpY x0 = face (edge ecpY) by rewrite /= nodeK (negPf x0gt1). rewrite !inE !unfold_in /= !orbF !(cface_icpN ecpY) orbA; congr (_ || _). by rewrite cfaceC; apply: (@same_cface ecpY); rewrite cface_icpY fconnect1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)