proposition: Lemma neighborUr A B C : neighbor A C -> neighbor A (B :|: C).
proof: Proof. apply: neighborW => //. exact: subsetUr. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)