proposition: Lemma finite_or_infinite x: cardinalp x -> finite_c x \/ infinite_c x.
proof: Proof. move => cx; move: (proj1 cx) => ox. by case: (p_or_not_p (infinite_o x)) => h; [ right | left ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)