proposition: Lemma neighbor_split (G : sgraph) (A B C1 C2 : {set G}) : B \subset C1 :|: C2 -> neighbor A B -> neighbor A C1 || neighbor A C2.
proof: Proof. move/subsetP => S /neighborP [u] [v] [? /S H E]. apply/orP. by case/setUP : H => ?; [left|right]; apply/neighborP; exists u; exists v. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)