proposition: Lemma connectedTE (G : sgraph) : connected [set: G] -> forall x y : G, connect (--) x y.
proof: Proof. move => A x y. move: (A x y). rewrite !inE !restrictE; first by apply. by move => ?; rewrite !inE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)