proposition: Lemma connected_restrict (G : sgraph) (A : pred G) x : connected [set y | connect (restrict A (--)) x y].
proof: Proof. move => u v. rewrite !inE => Hu Hv. move defP : (mem _) => P. wlog suff W: u Hu / connect (restrict P (--)) x u. { apply: connect_trans (W _ Hv). rewrite srestrict_sym. exact: W. } case: (altP (x =P u)) => [-> //|xDu]. case/connect_irredRP : Hu => // p Ip Ap. apply connectRI with p => z in_p. rewrite -defP inE. case/psplitP : in_p Ap => p1 p2 Ap. apply connectRI with p1. apply/subsetP. apply: subset_trans Ap. exact: subset_pcatL. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)