proposition: Fact embr_face_subproof (w : rdart) : embr_face (val w) \notin rdom'.
proof: Proof. rewrite /embr_face; have [u /andP[bGd_u /eqP/(canRL e2m) Dw] | bGd'ew] := pickP. by rewrite Dw /= (mem_image embdd_inj) -(fclosed1 bGd'E) negbK. apply/imageP=> [] [u /= bGd'u fdw]; have /andP[] := bGd'ew (node u). have Dew: edge (val w) = embdd (node u). by rewrite (canRL edgeK (e2m _)) fdw embddN. rewrite [_ \in _](contraR _ (embr_edge_subproof w)) ?Dew //. by rewrite (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)