proposition: Lemma outer_hd xd : (hd xd \in outer) = (xd \in Fbd).
proof: Proof. apply/idP/idP. case/exists_inP=> /= _ /connectP[p xFp ->]. elim: p xd xFp => [|y p IHp] xd /= => [_ | /andP[]]. by rewrite EbGdr => /(subsetP (ring_fband _)). have [b_xd | b'xd] := boolP (xd \in bGd). by rewrite (subsetP (ring_fband _)). rewrite -hdF // => /eqP <-; rewrite [xd \in _](eq_has (cface1 xd)). exact: IHp. case/hasP=> zd b_zd xFzd; case/connectP: xFzd b_zd => p xdFp ->{zd}. elim: p xd xdFp => [|yd p IHp] xd /= => [_ b_xd | /andP[/eqP <- {yd}]]. by apply: (subsetP (subset_closure _ _)); rewrite EbGdr. have [b_xd | b'xd] := boolP (xd \in bGd). by rewrite (subsetP (subset_closure _ _)) ?EbGdr. by rewrite (closure_closed cfaceC _ (eqxx _)) -hdF //; apply: IHp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)