proposition: Lemma sub_connect_to (a b : pred V) : a \subset b -> subrel (connect_to a) (connect_to b).
proof: Proof. move=> /subsetP sub_ab; apply: connect_sub => x y. by move=> /andP[/sub_ab ??]; apply: connect_to1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin