proposition: Lemma closure_closed a : closed e (closure e a).
proof: Proof. apply: intro_closed => x y /connect1 e_xy; congr (~~ _). by apply: eq_disjoint; apply: same_connect. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)