fact: Definition join_rel (a b : G1 + G2) := match a,b with | inl x, inl y => x -- y | inr x, inr y => x -- y | _,_ => false end.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)