proposition: Lemma fproj_cface x y : cface x y -> fproj x = fproj y.
proof: Proof. move=> xFy; rewrite /fproj (rootP cfaceC xFy); congr (nth _ p _). exact/eq_find/(same_cface xFy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)