proposition: Lemma add_edge_irrefl_ (G:sgraph) (i o : G) : irreflexive (add_edge_rel i o).
proof: Proof. move => x /=. by rewrite sg_irrefl eqxx. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)