proposition: Lemma adjnF_ecpN : fun_adjunction icpN face face ecpN.
proof: Proof. pose h := match _ with Icp x => x | IcpX => x0 | _ => edge (face (edge x0)) end. apply: (intro_adjunction cfaceC _ (fun u _ => h u)) => //= [|x _]; last first. split=> // _ /eqP <-; rewrite (@cface1 ecpN) /=; case: eqP => [-> | _]. rewrite (@cface1 ecpN) /=; case: ifP => // /eqP->. by rewrite nodeK fconnect1. by case: eqP => // ->; rewrite nodeK fconnect1. case=> [||x] /= _. - by split=> [|_ _ /eqP<- //]; rewrite fconnect1. - split=> [|_ _ /eqP<-]; first by rewrite (@cface1r ecpN) /= eqxx. by case: ifP => [_ | /eqP->]; rewrite cface1 ?nodeK. by split=> // _ _ /eqP <-; do 2?case: eqP => [-> | ] //=; rewrite cface1 ?nodeK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)