proposition: Lemma embed_inj : {in bc &, injective h1}.
proof: Proof. have bc_acN x: bc x -> x \notin ac -> edge x \notin ac -> node x \in ac. move=> bc_x ac'x ac'ex; case: (embed_cases x) => [/orP/norP|] [] // ac_enx. have bc_ex: edge x \in bc by rewrite inE /= (fclosed1 rcN) [~~ _]ac_bc. by have /norP[] := chordless_perimeter bc_x bc_ex. move=> x y; without loss ac_x: x y / x \in ac. move=> IH bc_x bc_y eq_hxy. have [ac_x | ac'x] := boolP (x \in ac); first exact: IH. have [ac_y | ac'y] := boolP (y \in ac); first exact/esym/IH. have [ac_nx | ac'nx] := boolP (node x \in ac). by apply/nodeI/IH; rewrite ?embedN ?eq_hxy // inE /= -(fclosed1 rcN). have [ac_ny | ac'ny] := boolP (node y \in ac). by apply/nodeI/esym/IH; rewrite ?embedN ?eq_hxy // inE /= -(fclosed1 rcN). by apply/edgeI/IH; rewrite ?embedE ?eq_hxy ?ac_bc ?(contraR (bc_acN _ _ _)). move=> bc_x bc_y; rewrite /h1 ac_x. have [|ac'y] := ifPn; first exact: pre_embed_inj. have [ac_ey | ac'ey] := ifPn; first by move/esym/embed_full <-; rewrite ?e2c. have ac_ny: node y \in ac by apply: bc_acN. have ac_enx: edge (node x) \in ac by rewrite (fclosed1 acF) nodeK. rewrite bc_acN // -{1}[x]nodeK hF // => /faceI h_enx. exact/esym/nodeI/edgeI/embed_full. 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)