proposition: Lemma fband_icpH u : {x | cface u (icpH x)} + {cface ecpH u}.
proof: Proof. have [v uFv] := fband_icpN u; have [[x vFx] | XFv] := fband_icpY v. by left; exists x; rewrite (same_cface uFv) cface_icpN. by right; rewrite cface1 (same_connect_r cfaceC uFv) cface_icpN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)