proposition: Lemma finite_compact {X : topologicalType} (A : set X) : finite_set A -> compact A.
proof: Proof. case/finite_setP=> n; elim: n A => [A|n ih A /eq_cardSP[x Ax /ih ?]]. by rewrite II0 card_eq0 => /eqP ->; exact: compact0. by rewrite -(setD1K Ax); apply: compactU => //; exact: compact_set1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed