proposition: Lemma cantor_bis: non_coll cardinalp.
proof: Proof. move=> [a ap]. have ca: cardinal_set a by move => t /ap. case: (cltNge (cantor (CS_sup ca))); apply: (card_sup_ub ca); apply/ap; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)