proposition: Lemma connected_in_subgraph (G : sgraph) (S : {set G}) (A : {set induced S}) : connected A -> connected [set val x | x in A].
proof: Proof. move => conn_A ? ? /imsetP [/= x xA ->] /imsetP [/= y yA ->]. case: (boolP (x == y)) => [/eqP->|Hxy]; first exact: connect0. move: (conn_A _ _ xA yA) => /connect_irredRP. move/(_ Hxy) => [p irr_p /subsetP subA]. case: (Path_from_induced p) => q sub_S Hq. apply: (connectRI q) => z. rewrite in_collective Hq => /mapP[z'] /subA Hz' ->. exact: imset_f. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)