fact: Definition ecpA_face x := if cface (edge x0) (node x0) then face x else if x == edge x0 then node x0 else if face x == node x0 then face (edge x0) else face x.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)