proposition: Lemma closure_connect e a x y : connect e x y -> y \in closure e a -> x \in closure e a.
proof: Proof. move => e_xy /closureP [z z_a c_yz]; apply/closureP ; exists z => //. exact: connect_trans c_yz. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)