proposition: Lemma closure1 e x : connect_sym e -> connect e x =i closure e (pred1 x).
proof: Proof. move => sym_e z; apply/idP/idP => [c_x_z|/closureP [x0] /eqP ->]; last by rewrite sym_e. by apply/closureP; exists x; rewrite ?inE // sym_e. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)