proposition: Lemma connect1r (g : rel V) x z : connect g x z -> z != x -> exists2 y, connect g x y & g y z.
proof: Proof. move=> xz zNx; move: xz; rewrite connect_rev => /connect1l. by rewrite eq_sym => /(_ zNx) [y]; exists y; rewrite // connect_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect)