proposition: Lemma connected_in_components (G : sgraph) (H C : {set G}) : C \in components H -> connected C.
proof: Proof. have PEQ := pblock_equivalence_partition (@sedge_equiv_in G H). move => C_comp. case/and3P: (partition_components H) => /eqP compU compI comp0. have/set0Pn [x in_C] : C != set0. by apply: contraNN comp0 => /eqP<-. have CH: {subset C <= H}. { move => z Hz. rewrite -compU. apply/bigcupP; by exists C. } move/CH : (in_C) => in_H. suff -> : C = [set y in H | connect (restrict H (--)) x y]. { exact: connected_restrict_in. } apply/setP => y. rewrite inE. case: (boolP (y \in H)) => /= [y_in_H|y_notin_H]. - by rewrite -PEQ // ?(def_pblock _ C_comp). - apply: contraNF y_notin_H. exact: CH. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)