fact: Definition cube_edge (u : cube_dart) := let: (o, x) := u in match o with | CTen => tsI CTnf (edge x) | CTf => tsI CTe (node (face x)) | CTnf => tsI CTen (node (face x)) | CTe => tsI CTf (edge x) | CTfe => tsI CTn x | CTn => tsI CTfe x end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring)