proposition: Lemma cl_sg_sym : symmetric (@dominates G).
proof: Proof. rewrite /symmetric /dominates /closed_neigh => x y ; by rewrite sg_sym eq_sym. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)