proposition: Lemma add_node_irrefl : irreflexive add_node_rel.
proof: Proof. move => [a|] //=. by rewrite sgP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)