proposition: Lemma connected1 (G : sgraph) (x : G) : connected [set x].
proof: Proof. move => ? ? /set1P <- /set1P <-. exact: connect0. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)