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