proposition: Lemma closureP e a y : reflect (exists2 x, x \in a & connect e y x) (y \in closure e a).
proof: Proof. rewrite /closure_mem unfold_in disjoint_sym. by apply: (iffP pred0Pn) => [[x] /andP[? ?]|[x]]; exists x. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)