proposition: Fact embr_node_subproof (w : rdart) : embr_node (val w) \notin rdom'.
proof: Proof. rewrite /embr_node; have [u /andP[bGd_u /eqP Dw] | bGd'w] := pickP. by rewrite Dw /= (mem_image embdd_inj) (fclosed1 bGd'E) faceK negbK. apply/imageP=> [] [u /= bGd'u ndw]; have /andP[] := bGd'w (node (node u)). have Dw: val w = embdd (node (node u)) by rewrite !embddN -ndw n3m. by rewrite [_ \in _](contraR _ (valP w)) ?Dw // (mem_image embdd_inj). 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)