proposition: Lemma embedE : {morph h1 : x / edge x}.
proof: Proof. move=> x; wlog bc_x: x / x \in bc. move=> IH; case: (orP (edge_perimeter x)) => /IH //. by rewrite e2c => ->; rewrite e2m. rewrite /h1 e2c; do 2!case: ifPn; rewrite ?e2m //; first exact: embed_functor. move=> ac'x ac'ex; have [/orP/norP[]//|/orP] := embed_cases x. case: ifPn => [ac_nex _ | ac'nex]; last first. by rewrite orbF (canRL nodeK (n3m _)) => ->. have bc_ex: edge x \in bc by rewrite inE /= (fclosed1 rcN); apply: ac_bc. by have /norP[] := chordless_perimeter bc_x bc_ex. 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)