proposition: Lemma cface_icpA (x y : G) : (cface : rel ecpA) x y = cface x y || all (mem (fband [:: face (edge x0); node x0])) [:: x; y].
proof: Proof. set a := fband _. have [_ eqFa']: fun_adjunction (id : ecpA -> G) face face [predC a]. have clFa: fclosed face [predC a] by apply: predC_closed; apply: fbandF. apply: {x y} (strict_adjunction cfaceC) => // [|x y /negbNE/= a'x]. by apply/subsetP => x _; apply: codom_f. apply/esym/baseF_ecpA; rewrite /icpA; apply: contra a'x => /pred2P[] -> /=. by rewrite unfold_in /= fconnect1. by rewrite unfold_in /= orbCA cface1 nodeK connect0. rewrite orbC /=; have [| /eqFa'-> //] := boolP (x \in a). have [| a'y] := boolP (y \in a); last by rewrite cfaceC (@cfaceC ecpA) eqFa'. rewrite !unfold_in => /hasP[t Dt yFt] /hasP[z Dz xFz] /=. apply: {x xFz}(connect_trans (sub_cface_icpA xFz)). rewrite cfaceC {y yFt}(same_cface (sub_cface_icpA yFt)). move: ecpA_merge Dz Dt; rewrite edgeK !inE => fex0Fnx0. by case/pred2P=> -> /pred2P[]-> //; rewrite cfaceC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)