proposition: Lemma edge_central_edge : plain G -> plain G' -> forall x, edge_central (edge x) = edge_central x.
proof: Proof. move=> plainG plainG' x; rewrite /= eq_sym plain_eq //. by rewrite (canF_eq (plain_eq plainG')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)