proposition: Lemma connectedTI (G : sgraph) : (forall x y : G, connect (--) x y) -> connected [set: G].
proof: Proof. move => H x y _ _. rewrite restrictE // => z. by rewrite inE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)