proposition: Lemma connect_toW a : subrel (connect_to a) (connect r).
proof: Proof. by apply/(@sub_connect_to _ predT)/subsetP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin