proposition: Lemma closed_connect a : closed e a -> forall x y, connect e x y -> (x \in a) = (y \in a).
proof: Proof. move=> cl_a x _ /connectP[p e_p ->]. by elim: p x e_p => //= y p IHp x /andP[/cl_a->]; apply: IHp. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)