proposition: Lemma pre_embed_inj : {in ac &, injective h}.
proof: Proof. move=> x y ac_x ac_y /= Dhx; have ac_eex: edge (edge x) \in ac by rewrite e2c. have [[|z1 [|z2 p]] [//=/andP[xFz1 z1Rp] Lp _] [_ p_ac]] := h_spoke ac_eex ac_y. by apply: cface_inj_embed; rewrite // -[x]e2c (same_cface xFz1). have [z1Rz2 _] := andP z1Rp; rewrite /rlink e2c in xFz1. have [/andP[ac_z1 /eqP hez1] /andP[ac_z2 _] _] := and3P p_ac. have hxFhz1 := cface_ac_h ac_x xFz1; rewrite Dhx in hxFhz1. have [t yFt Dht] := cface_h_ac ac_y hxFhz1. have ac_t: t \in ac by rewrite -(closed_connect acF yFt). have ac_ez1: edge z1 \in ac by rewrite (closed_connect acF z1Rz2). apply: cface_inj_embed; rewrite // (same_cface xFz1) cfaceC. by rewrite -(edgeI (embed_full ac_t ac_ez1 _)) // Dht. 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)