proposition: Theorem cantor a: cardinalp a -> a <c (\2c ^c a).
proof: Proof. move=> ca; rewrite - card_setP. rewrite - {1} (card_card ca). split. apply /eq_subset_cardP1. exists (Lf singleton a (\Po a)); hnf; saw. apply: lf_injective. by move=> t ta /=; apply/setP_P => v /set1_P ->. by move=> u v ua va; apply: set1_inj. apply/ card_eqP; move => [f [[_ suf] sf tf]]. set (X:= Zo a (fun x => (~ inc x (Vf f x)))). have Xt: (inc X (target f)) by rewrite tf; apply /setP_P; apply: Zo_S. move: ((proj2 suf) _ Xt) => [y ysf Wy]. have:(~ (inc y X)) by move=> yX; move: (yX) => /Zo_hi;rewrite - Wy. move=> h;case: (h); apply: Zo_i; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)