proposition: Lemma embedqz_arity x : x \in ac -> arity (h x) = arity x.
proof: Proof. have [_ /eqseqP qz_x0c _ <-] := qz_ok; rewrite /h => s0cFx. set i := find (cface x) s0c; set y := nth x0c s0c i; set j := findex face y x. have lti: i < size s0c by rewrite -has_find. have s0_y: y \in s0c by apply: mem_nth. have xFy: cface x y by apply: nth_find. rewrite (arity_cface xFy) /y -(nth_map x0c 0) // -qz_x0c (eqseqP qz_x0m) -/s0m. rewrite (nth_map x0m); last by rewrite !size_walkqz in lti *. by elim: j => //= j <-; rewrite arity_face. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)