proposition: Lemma cle1P E: \1c <=c (cardinal E) <-> nonempty E.
proof: Proof. split. move => h; case: (emptyset_dichot E) => // h1. case:(cleNgt h); rewrite h1 (cardinal_set0); exact:clt_01. move=> /card_nonempty1 nE; apply: cge1;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)