proposition: Lemma fbandF : fclosed face fband.
proof: Proof. apply: (intro_closed cfaceC) => x _ /eqP <- /hasP[z pz xFz]; apply/hasP. by exists z; last by rewrite -cface1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)