proposition: Lemma czero_dichot x: cardinalp x -> x = \0c \/ \0c <c x.
proof: Proof. move => ox; case: (equal_or_not x \0c) => xz; [by left | right]. split; [ exact:cle0x | exact:nesym]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)