proposition: Lemma nexts1_split (A : {set V}) x : x \in A -> nexts A [set x] = x |: nexts (A :\ x) (successors x).
proof: Proof. move=> xA; apply/setP=> y; apply/idP/idP; last first. rewrite nexts1 !inE xA; case: (_ == _); rewrite //=. by apply: subsetP; rewrite sub_nexts// subsetDl. move=> /bigcupP[z]; rewrite !inE => /eqP {z}->. move=> /connectP[p /shortenP[[_ _ _ /eqP->//|z q/=/andP[/andP[_ xz]]]]]. rewrite path_from => /andP[zq] /allP/= qA. move=> /and3P[xNzq _ _] _ ->; apply/orP; right. apply/bigcupP; exists z; rewrite !inE//. apply/connectP; exists q; rewrite // path_from zq/=. apply/allP=> t tq; rewrite !inE qA ?andbT//. by apply: contraNneq xNzq=> <-; apply: mem_belast tq. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors