proposition: Lemma finiteP (E : pred T) : (exists s : seq T, {subset E <= s}) -> finite E.
proof: Proof. case/cid=> s sEs; exists (undup s); first by rewrite undup_uniq. by move=> x; rewrite mem_undup; exact: sEs. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals