proposition: Lemma embedqz_face : {in ac, {morph h : x / face x}}.
proof: Proof. move=> x ac_x; have [_ _ _ Dac] := qz_ok; rewrite /h -(eq_find (cface1 x)). set i := find _ s0c; rewrite -Dhs0; set yc := nth _ s0c i. have s0cFx: x \in fband s0c by rewrite Dac. have ycFx: cface yc x by rewrite cfaceC (nth_find _ s0cFx). rewrite -{1}(iter_findex ycFx) -!iterS. have:= findex_max ycFx; rewrite leq_eqVlt. case/predU1P=> [-> | /findex_iter->//]; rewrite (iter_order faceI) findex0 /=. by rewrite -embedqz_arity ?(iter_order faceI) ?(closed_connect acF ycFx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)