proposition: Lemma simple_cface : simple -> {in p &, forall x y, cface x y -> x = y}.
proof: Proof. move=> Up x y px py xFy. by rewrite -(simple_fproj Up px) (fproj_cface xFy) simple_fproj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)