fact: Definition sew_face_r (xr : Gr) : sew_dart := match sewr (face xr) with | existT SewDisk xd => sewd (face xd) | ufr => ufr end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color patch)