proposition: Lemma cface_embd : {mono embd : u v / cface u v}.
proof: Proof. move=> u v; apply/idP/idP=> /connectP[p]; last first. move=> uFp -> {v}; elim: p u uFp => //= v p IHp u /andP[Dv /IHp]. apply: connect_trans; rewrite -(eqP Dv) /embd /= /embd_face. by case: ifP => _; rewrite -!cface1r. elim: {p}_.+1 u {-2}p (ltnSn (size p)) => // n IHn u [|y p] lepn. by move=> _ Dv; apply/eq_connect0/embd_inj. rewrite cface1 /= => /andP[/eqP Dy yFp] Lp. have{IHn}:= IHn (face u); rewrite /= /embd_face Dy. have [bc_y | bc'y] := ifP; first by move/(_ p)->. case: p => [|z p] /= in yFp Lp lepn *; first by rewrite -Lp (valP v) in bc'y. by case/andP: yFp => /eqP-> zFp; move/(_ p) => -> //; apply: ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)