proposition: Lemma neighbor_connected A B : connected A -> connected B -> neighbor A B -> connected (A :|: B).
proof: Proof. move => conA conB /neighborP [x] [y] [? ? xy]. exact: connectedU_edge xy _ _. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)