proposition: Lemma fband_cons x p y : (y \in fband (x :: p)) = cface y x || (y \in fband p).
proof: Proof. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)