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