fact: Record patch : Prop := Patch { patch_injd : injective hd; patch_injr : injective hr; patch_cycle_d : sfcycle edge bGd; patch_cycle_r : ufcycle node bGr; patch_map_ring_r : map hr bGr = rev (map hd bGd); patch_codom_r : codom hr =i [predU [predC codom hd] & map hd bGd]; patch_edge_d : {in [predC bGd], {morph hd : xd / edge xd}}; patch_node_d : {morph hd : xd / node xd}; patch_edge_r : {morph hr : xr / edge xr}; patch_node_r : {in [predC bGr], {morph hr : xr / node xr}} }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)