proposition: Lemma fproj_cat p1 p2 x : fproj (p1 ++ p2) x = fproj (if x \in fband p1 then p1 else p2) x.
proof: Proof. elim: p1 => [|y p1 IHp1] //=; rewrite fband_cons cfaceC fproj_cons IHp1. by case: ifP => yFx /=; last case: ifP => // _; rewrite fproj_cons yFx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)