proposition: Lemma nexts1 x : nexts [set x] = x |: (if x \in D then nexts [set y in successors x] else set0).
proof: Proof. apply/setP=> y; rewrite /nexts big_set1 !inE. have [->|neq_yx/=] := altP eqP; first by rewrite connect0. apply/idP/idP=> [/connect1l[]// z/=/andP[/= xD xz zy]|]. by rewrite xD; apply/bigcupP; exists z; rewrite !inE. case: ifPn; rewrite ?inE// => xD /bigcupP[z]; rewrite !inE. by move=> xz; apply/connect_trans/connect1; rewrite /= xD. Qed.
imports: mathcomp(all_ssreflect) bigmin extra