proposition: Lemma connected_component_trans A y x z : connected_component A x y -> connected_component A y z -> connected_component A x z.
proof: Proof. move=> [B [Bx BA Ac Ay]] [C [Cy CA Cc Cz]]; exists (B `|` C); last by right. by split; [left | rewrite subUset | apply: connectedU=> //; exists y]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed