proposition: Lemma connected_restrict_in (G : sgraph) (A : pred G) x : x \in A -> connected [set y in A | connect (restrict A (--)) x y].
proof: Proof. move => inA. rewrite -connect_range //. exact: connected_restrict. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)