fact: Definition sew_face (w : sew_dart) : sew_dart := match w with | existT SewDisk xd => if in_bGd xd is inleft ur then sew_face_r (hdr (sval ur) xd) else sewd (face xd) | existT SewRest ur => sew_face_r (sval ur) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color patch)