proposition: Lemma add_edgeC (G : sgraph) (s1 s2 : G): @edge_rel (add_edge s1 s2) =2 @edge_rel (add_edge s2 s1).
proof: Proof. move => x y. rewrite /edge_rel /= [y == x]eq_sym. by case (x -- y) => //=; do ! (case (_ == _); rewrite //=). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)