proposition: Lemma fband_cat p1 p2 x : (x \in fband (p1 ++ p2)) = (x \in fband p1) || (x \in fband p2).
proof: Proof. exact: has_cat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)