proposition: Lemma finiteNP (E : pred T): (forall s : seq T, ~ {subset E <= s}) -> forall n, exists s : seq T, [/\ size s = n, uniq s & {subset s <= E}].
proof: Proof. move=> finN; elim=> [|n [s] [<- uq_s sE]]; first by exists [::]. have [x sxN xE]: exists2 x, x \notin s & x \in E. apply: contra_notP (finN (filter (mem E) s)) => /forall2NP finE x Ex. move/or_asboolP: (finE x). by rewrite !asbool_neg !asboolb negbK Ex mem_filter orbF [(mem E) x]Ex. exists (x :: s) => /=; rewrite sxN; split=> // y. by rewrite in_cons => /orP[/eqP->//|/sE]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals