proposition: Lemma connect_to1 (a : pred V) x y : y \in a -> r x y -> x -[a]-> y.
proof: Proof. by move=> ay Rxy; rewrite connect1 //= ay. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin