proposition: Lemma neighborW C D A B : C \subset A -> D \subset B -> neighbor C D -> neighbor A B.
proof: Proof. move/subsetP => subA /subsetP subB /neighborP [x] [y] [? ? ?]. apply/neighborP; exists x; exists y. by rewrite subA ?subB. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)