proposition: Lemma plain_eq' : plain -> forall x, node (face x) = edge x.
proof: Proof. by move=> plainG x; rewrite -{2}[x]faceK plain_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)