proposition: Lemma finite_or_infinite_set x: finite_set x \/ infinite_set x.
proof: Proof. case:(finite_or_infinite (CS_cardinal x)); first by left. by move/infinite_setP; right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)