proposition: Lemma add_edge_sym_ (G:sgraph) (i o : G) : symmetric (add_edge_rel i o).
proof: Proof. apply: relU_sym'. exact: sg_sym. exact: sc_sym. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)