proposition: Lemma connect_range (G : sgraph) (A : pred G) x : x \in A -> [set y | connect (restrict A (--)) x y] = [set y in A | connect (restrict A (--)) x y].
proof: Proof. move => inA. apply/setP => z. rewrite !inE srestrict_sym. apply/idP/andP => [|[//]]. by case/connect_restrict_case => [->|[]]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)