fact: Definition sewr_r xr b'xr : sew_dart := @Tagged _ SewRest sew_dart_at (sub xr b'xr).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color patch)