proposition: Lemma adjnF_ecpU : fun_adjunction icpU face face (predC1 (ecpU : ecpU)).
proof: Proof. pose h u (_ : predC1 (ecpU : ecpU) u) := if u is Icp x then x else node x0. apply: (intro_adjunction cfaceC closedF_ecpU h) => [|x /= _]; last first. split=> // _ /eqP <-; rewrite (@cface1 ecpU) /=. by case: eqP => // ->; apply: fconnect1. case=> [||x] //= _. by split; [apply: fconnect1 | case=> //= y _ /(_ =P y) <-]. split=> // [] [||y] //= _; case: (face x =P _) => //. by move=> <- _; apply: fconnect1. by move=> _ /(_ =P y) <-; apply: fconnect1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)