proposition: Lemma connect_from (a : pred V) (g : rel V) x z : connect g x z -> exists y, [/\ (y \in a) ==> (z == y) && (z \in a), connect (relfrom a g) x y & connect g y z].
proof: Proof. rewrite connect_rev => cgxz; have [y [ayaz]]//= := connect_to a cgxz. by exists y; split; rewrite // connect_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect)