proposition: Lemma fproj_cons x p y : fproj (x :: p) y = (if cface x y then x else fproj p y).
proof: Proof. by rewrite /fproj /= cfaceC; case: ifP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)