proposition: Lemma add_edge_no_isolated (G : sgraph) (x y : G) : no_isolated G -> no_isolated (add_edge x y).
proof: Proof. by move => no_isoG u; have [v uv] := no_isoG u; exists v; rewrite /edge_rel/= uv. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)