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