proposition: Lemma adj_ecpU u : adj ecpU u = (u \in fband [:: icpU (node x0)]).
proof: Proof. rewrite /adj /orbit /order (eq_card cface_ecpU) (card1 ecpU) /=. by rewrite /rlink cface1 cfaceC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)