proposition: Lemma add_edge_sym (G : sgraph) (s1 s2 : G): diso (@add_edge G s1 s2) (@add_edge G s2 s1).
proof: Proof. apply: eq_diso. exact: add_edgeC. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)