proposition: Lemma connected2 (G : sgraph) (x y: G) : x -- y -> connected [set x; y].
proof: Proof. move=> xy ? ? /set2P[]-> /set2P[]->; try exact: connect0. all: apply: connect1; rewrite /= !inE !eqxx orbT //=; by rewrite sg_sym. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)