proposition: Lemma codom_embd : codom embd =i bc.
proof: Proof. move=> x; apply/imageP/idP => [[u _ ->] | bc_x]; first exact: (valP u). by exists (sub x bc_x). 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)