proposition: Lemma patch_face_d' xd yd : cface xd yd -> cface (hd xd) (hd yd).
proof: Proof. case/connectP=> p xFp ->{yd}. by elim: p xd xFp => //= _ p IHp xd /andP[/eqP <- /IHp]; apply: connect_trans. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)