proposition: Lemma connected_induced (G : sgraph) (S : {set G}) : connected S -> connected [set: induced S].
proof: Proof. move => conn_S x y _ _. rewrite restrictE => [|u]; last by rewrite inE. have/connect_irredRP := conn_S _ _ (valP x) (valP y). case: (boolP (val x == val y)) => [|E /(_ isT) [p] _ /subsetP sub_S]. - rewrite val_eqE => /eqP-> _. exact: connect0. - case: (Path_to_induced sub_S) => q _. exact: Path_connect q. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)