proposition: Lemma sg_edgeNeq (G : sgraph) (x y : G) : x -- y -> (x == y = false).
proof: Proof. apply: contraTF => /eqP ->. by rewrite sg_irrefl. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)