proposition: Fact embed_disk_subproof : cancel3 dedge dnode dface.
proof: Proof. move=> u; apply: val_inj; rewrite /= /embd_edge. case: ifP => [bc_ex | bc'ex]; last by rewrite /embd_face nodeK bc'ex edgeK. by rewrite /embd_face inE /= (fclosed1 rcN) edgeK [~~ _](valP u) 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)