proposition: Lemma nextsUI A B C : nexts B A \subset A -> A :|: nexts (B :&: ~: A) C = A :|: nexts B C.
proof: Proof. move=> subA; apply/setP=> y; rewrite !inE; have [//|/= yNA] := boolP (y \in A). apply/idP/idP; first by apply: subsetP; rewrite sub_nexts// subsetIl. move=> /bigcupP[z zr zy]; apply/bigcupP; exists z; first by []. rewrite !inE; apply: contraTT isT => Nzy; move: zy; rewrite !inE. move=> /(connect_from (mem (~: A))) /= [t]. rewrite !inE => -[xtxy zt ty]; move: zt. rewrite (@eq_connect _ _ (relfrom (mem (B :&: ~: A)) edge)); last first. by move=> u v /=; rewrite !inE andbCA andbA. case: (altP eqP) xtxy => /= [<-|neq_yt]; first by rewrite (negPf Nzy). rewrite implybF negbK => tA zt; rewrite -(negPf yNA) (subsetP subA)//. by apply/bigcupP; exists t; rewrite // inE. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors