proposition: Lemma baseF_ecpA : fun_base icpA face face (pred2 (edge x0) (edge (node (node x0)))).
proof: Proof. move=> x y; rewrite /icpA /= /ecpA_face => /norP[ex0'x ennx0'x]. by rewrite (negPf ex0'x) (canF_eq faceK) (negPf ennx0'x) if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)