proposition: Lemma intro_closed a : (forall x y, e x y -> x \in a -> y \in a) -> closed e a.
proof: Proof. move=> cl_a x y e_xy; apply/idP/idP=> [|a_y]; first exact: cl_a. have{x e_xy} /connectP[p e_p ->]: connect e y x by rewrite sym_e connect1. by elim: p y a_y e_p => //= y p IHp x a_x /andP[/cl_a/(_ a_x)]; apply: IHp. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)