proposition: Lemma precompactE (C : set X) : precompact C = compact (closure C).
proof: Proof. rewrite propeqE; split=> [[B CsubB [cptB cB]]|]; last first. move=> clC; exists (closure C) => //; first exact: subset_closure. by split => //; exact: closed_closure. apply: (subclosed_compact _ cptB); first exact: closed_closure. by move/closure_id: cB => ->; exact: closure_subset. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed