proposition: Fact embr_edge_subproof (w : rdart) : edge (sval w) \notin rdom'.
proof: Proof. apply: contra (valP w) => /= /imageP[u bGd'u /(canRL e2m)->{w}]. by rewrite -embddE // image_f // -(fclosed1 bGd'E). 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)