proposition: Lemma precompact_subset (A B : set X) : A `<=` B -> precompact B -> precompact A.
proof: Proof. by move=> AsubB [B' B'subB cptB']; exists B' => // ? ?; exact/B'subB/AsubB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed