proposition: Lemma quiz_preembedding : preembedding ac h.
proof: Proof. split; last exact: embedqz_rlinked. - exact: embedqz_face. - exact: embedqz_arity. have [_ _ _ Dac] := qz_ok. apply/subsetP=> x; rewrite -Dac => /hasP[y s0_y xFy]. by apply/exists_inP; exists y => //=; apply: embedqz_central. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)