proposition: Lemma connect_to_forced (a : pred V) x y : (forall z, z != x -> x -[]-> z -> z -[]-> y -> a z) -> x -[]-> y -> x -[a]-> y.
proof: Proof. move=> Hf /connectP[p {p}/shortenP[p Hp Up _ Hy]]. apply/connectP. elim: p {-2 4}x Hy Up Hp (connect0 (relto a r) x) => [z /=-> _ _ Hz| z p IH /= z1 Hy /and3P[H1 H2 H3] /andP[Rxy Pp] Hz1]. by exists [::]. move: H1; rewrite inE negb_or => /andP[xDz H1]. have Az : a z. apply: Hf; first by rewrite eq_sym. apply: connect_trans (connect_toW Hz1) (connect1 Rxy). by apply/connectP; exists p. have Raz : x -[a]-> z. by apply: connect_trans Hz1 (connect_to1 Az Rxy). have Uxp : uniq (x :: p) by rewrite /= H1. have [p1 H1p1 H2p1] := IH _ Hy Uxp Pp Raz. by exists (z :: p1); rewrite //= [_ \in _]Az Rxy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin