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