proposition: Lemma connect_to (a : pred V) (g : rel V) x z : connect g x z -> exists y, [/\ (y \in a) ==> (x == y) && (x \in a), connect g x y & connect (relto a g) y z].
proof: Proof. move=> /connectP [p gxp ->]. pose P := [pred i | let y := nth x (x :: p) i in [&& connect g x y & connect (relto a g) y (last x p)]]. have [] := @ex_minnP P. by exists (size p); rewrite /= nth_last (path_connect gxp) //= mem_last. move=> i /= /andP[g1 g2] i_min; exists (nth x (x :: p) i); split=> //. case: i => [|i] //= in g1 g2 i_min *; first by rewrite eqxx /= implybb. have i_lt : i < size p. by rewrite i_min // !nth_last /= (path_connect gxp) //= mem_last. have [<-/=|neq_xpi /=] := altP eqP; first by rewrite implybb. have := i_min i; rewrite ltnn => /contraNF /(_ isT) <-; apply/implyP=> axpi. rewrite (connect_trans _ g2) ?andbT //; last first. by rewrite connect1 //= [_ \in _]axpi /= (pathP x _). by rewrite (path_connect gxp) //= mem_nth //= ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect)