proposition: Lemma cpow_less_pr5c x: \2c <=c x -> finite_c x -> x ^<c omega0 = omega0.
proof: Proof. move => x2 xf. have co:= CS_omega. have aux:= (@cpow_less_pr0 x omega0). have oic:= CIS_omega. have xb: natp x by apply /NatP. have le1: x ^<c omega0 <=c omega0. apply:card_ub_sup => // i /funI_P [z zx ->]. move: zx => /(cardinals_ltP co) zx. by apply: cle_fin_inf => //;apply /NatP; apply (NS_pow xb); apply/clt_omegaP. ex_middle neq1. set t := x ^<c omega0. have to: t <c omega0 by split. have pb:= (cantor (proj31_1 to)). case: (cleNgt (cpow_less_pr2 x to) (clt_leT pb (cpow_Mleeq t x2 card2_nz))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)