proposition: Lemma patch_face_d xd yd : ~~ outer (hd xd) -> cface xd yd = cface (hd xd) (hd yd).
proof: Proof. exact: (rel_functor adj_hd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)