proposition: Lemma simple_fproj : simple -> {in p, fproj =1 id}.
proof: Proof. rewrite /simple /fproj => Up x px; case/splitPr: px Up => p1 p2. rewrite map_cat cat_uniq /= => /and3P[_ /norP[p1'Fx _] _]. rewrite find_cat /= connect0 addn0. case: hasP => [[y py xFy] | _]; last by rewrite nth_cat ltnn subnn. by case/mapP: p1'Fx; exists y; rewrite ?(rootP cfaceC xFy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)