proposition: Lemma eq_symconnect_to (a b : pred V) x y : a =i b -> x =[a]= y = x =[b]= y.
proof: Proof. by move=> eq_ab; apply: eq_symconnect=> x1 y1; rewrite /= eq_ab. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin