proposition: Lemma sub_nexts (D D' A B : {set V}) : D \subset D' -> A \subset B -> nexts D A \subset nexts D' B.
proof: Proof. move=> /subsetP subD /subsetP subAB; apply/subsetP => v /bigcupP[a /subAB aB]. rewrite !inE => av; apply/bigcupP; exists a; rewrite ?inE //=. by apply: connect_sub av => x y /andP[xD xy]; rewrite connect1//= subD. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors