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