proposition: Fact add_edges2_sym : symmetric add_edges2_rel.
proof: Proof. by move=> x y; rewrite /= ![_ && (x \in _)]andbC [_ && _ || _]orbC eq_sym sg_sym. 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)