fact: Definition D4_node (x : 'I_n) : 'I_n := match val x with | 0 => 'd1 | 1 => 'd2 | 2 => 'd0 | 3 => 'd4 | 4 => 'd5 | 5 => 'd3 | 6 => 'd7 | 7 => 'd8 | 8 => 'd6 | 9 => 'd10 | 10 => 'd11 | 11 => 'd9 | _ => 'd0 end.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)