proposition: Lemma embedN : {in bc, {morph h1 : x / node x}}.
proof: Proof. move=> x bc_x; rewrite /h1 (fclosed1 acF (edge (node x))) nodeK. rewrite (canRL nodeK (n3c bc_x)) -(fclosed1 acF). have [ac_x | ac'x] := boolP (x \in ac). have ac_enx: edge (node x) \in ac by rewrite (fclosed1 acF) nodeK. apply: edgeI; rewrite -[x as x in h x]nodeK (hF ac_enx) faceK fun_if e2m. by case: ifP => // ac_nx; rewrite embed_functor. have [ac_ex | ac'ex] := boolP (edge x \in ac). case: ifPn => [ac_nx | ac'nx]; last first. by rewrite -(canRL nodeK (n3m _)) hF // (canRL edgeK (e2m _)). rewrite (canRL edgeK (e2m _)) -hF // -(canRL nodeK (n3c bc_x)). have ac_ennx: edge (node (node x)) \in ac by rewrite (fclosed1 acF) nodeK. rewrite (canRL nodeK (n3m _)) -embed_functor -?hF ?nodeK //. by rewrite (canRL nodeK (n3c bc_x)) -fclosed1. case: (embed_cases x) => /orP; first by case/norP. rewrite (fun_if node) edgeK; case: ifP => //= _ ac_nex. 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)