proposition: Lemma connect1l (g : rel V) x z : connect g x z -> z != x -> exists2 y, g x y & connect g y z.
proof: Proof. move=> /connectP [[|y p] //= xyp ->]; first by rewrite eqxx. by move: xyp=> /andP[]; exists y => //; apply/connectP; exists p. Qed.
imports: HB(structures) mathcomp(all_ssreflect)