proposition: Lemma countable_finite_or_N E: countable_set E -> finite_c (cardinal E) \/ cardinal E = aleph0.
proof: Proof. move /countableP => leB. case: (equal_or_not (cardinal E) aleph0) => ne; [by right | left]. apply/NatP; exact:(olt_i(oclt (conj leB ne))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)