proposition: Fact embed_rem_subproof : cancel3 redge rnode rface.
proof: Proof. move=> w; apply: val_inj; rewrite /= /embr_face e2m. have [u /andP[bGd_u /eqP->] | bGd'w] := pickP; rewrite /embr_node. have [_ /andP[_ /eqP/embdd_inj <-] | /(_ (edge u))] /= := pickP. by rewrite [dnode _](edgeK u). by rewrite -(fclosed1 bGdE) bGd_u eqxx. have [u /andP[bGd_u /eqP/= Dfew] | _] /= := pickP; last exact: edgeK. have /negP[]:= valP w; rewrite -[val w]edgeK Dfew -embddN image_f //. by apply: contraFN (bGd'w (node u)) => /= -> /=; rewrite embddN -Dfew edgeK. 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)