proposition: Lemma add_edge_connected_sym (G : sgraph) s1 s2 A: @connected (@add_edge G s1 s2) A <-> @connected (@add_edge G s2 s1) A.
proof: Proof. apply: eq_connected => u v. exact: (add_edgeC s1 s2). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)