proposition: Lemma in_nextsW A y : y \in nexts A -> exists2 x, x \in A & gconnect x y.
proof: Proof. move=>/bigcupP[x xA]; rewrite inE => xy; exists x => //. by apply: connect_sub xy => u v /andP[_ /connect1]. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors