proposition: Lemma nexts_id (A : {set V}) : nexts (nexts A) = nexts A.
proof: Proof. apply/eqP; rewrite eqEsubset nextsS andbT; apply/subsetP=> x. move=> /bigcupP[y /bigcupP[z zA]]; rewrite !inE => /connect_trans yto /yto zx. by apply/bigcupP; exists z; rewrite ?inE. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors