fact: Definition ecpU_face x := match x with | IcpX => IcpX G | IcpXe => Icp (node x0) | Icp y => if face y == node x0 then IcpXe G else Icp (face y) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)