proposition: Lemma cface_inj_embed x y : x \in ac -> cface x y -> h x = h y -> x = y.
proof: Proof. move=> ac_x xFy eq_hxy. have iter_hF n: h (iter n face x) = iter n face (h x). by elim: n (x) ac_x => // n IHn z ac_z; rewrite !iterSr -hF ?IHn -?fclosed1. have eq_iFxy: findex face (h x) (h y) = findex face x y. by rewrite -{1}(iter_findex xFy) iter_hF findex_iter // hFn // findex_max. by rewrite -(iter_findex xFy) -eq_iFxy eq_hxy findex0. 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)