fact: Definition D4_g (x : D4) : 'K_4 := match val x with | 0 => ord0 | 1 => ord0 | 2 => ord0 | 3 => ord1 | 4 => ord1 | 5 => ord1 | 6 => ord2 | 7 => ord2 | 8 => ord2 | 9 => ord3 | 10 => ord3 | 11 => ord3 | _ => ord0 end.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)