proposition: Lemma uncountable_set_infinite x: uncountable_set x -> infinite_set x.
proof: Proof. by move => h; case: (finite_or_infinite_set x) => // /finite_is_countable. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)