proposition: Lemma connected_component_id A x : A x -> connected A -> connected_component A x = A.
proof: Proof. move=> Ax Ac; apply/seteqP; split; first exact: connected_component_sub. by move=> y Ay; exists A => //; split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed