proposition: Lemma sedge_equiv (G : sgraph) : equivalence_rel (connect (@sedge G)).
proof: Proof. apply: equivalence_rel_of_sym. exact: sg_sym. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)