proposition: Lemma Nwreach e x : x \notin whites e -> wreach e x = [set x].
proof: Proof. move=> xNwhite; apply/eqP; rewrite eqEsubset sub1set mem_wreach andbT. apply/subsetP=> y; rewrite !inE => /connectP []. by move=> [|z p] /=; rewrite ?(negPf xNwhite) // => _ ->. Qed.
imports: mathcomp(all_ssreflect) bigmin extra