proposition: Lemma fband_icpU u : {x : G | cface u (icpU x)} + {cface ecpU u}.
proof: Proof. rewrite cface_ecpU; case: eqP; first by right. by case: u => // [|x] _; left; [exists (node x0); apply: fconnect1 | exists x]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)