fact: Definition add_node_rel (x y : option G) := match x,y with | None, Some y => y \in N | Some x, None => x \in N | Some x,Some y => x -- y | None, None => false end.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)