proposition: Lemma cantor_of_limit x: limit_ordinal x -> exists a n, [/\ ordinalp a, ordinalp n, n <> \0o, x = a +o (oopow n) & (a = \0o \/ [/\ limit_ordinal a, (oopow n) <=o a & cardinal x = cardinal a])].
proof: Proof. move/limit_ordinal_P => [xnz lx]. move: (CNFr_exists (proj32_1 xnz))=> [f [n [nN ax xv]]]. case: (equal_or_not n \0c) => nz. by case: xnz; rewrite xv /CNFrv -/n nz osum_f0. have ax0 := proj1 ax. have cn1: \1c <=c n by apply: cge1; fprops. move : (cdiff_pr cn1) (NS_diff \1c nN); set m := _ -c _ => nv mN. set f1 := (fun i => oopow (f i)). have ha: ord_below f1 (\1c +c m). move => i; rewrite nv => lin; apply:(OS_oopow (ax0 _ lin)). have hb: ordinalp (f \0c) by apply:ax0; apply/strict_pos_P1. have hc:= (OS_pow OS_omega hb). move: xv; rewrite /CNFrv -/n -nv. rewrite (osum_fA NS1 mN ha) (osum_f1 (f := f1) hc) {2} /f1. rewrite -/(CNFrv _ _); set f2:= (fun i : Set => f (i +c \1c)). have ax3: CNFr_ax f2 m. split. move => i im; apply: ax0; rewrite - nv (csumC \1c). apply:csum_Mlteq; fprops. move => i iN sim. have eq: (csucc i +c \1c) = csucc (i +c \1c) by rewrite (csum_Sn _ iN). rewrite /f2 eq; apply:(proj2 ax); first by apply:(NS_sum iN NS1). rewrite - nv (csumC \1c) - eq; apply:csum_Mlteq; fprops. move:(OS_CNFr0 mN ax3); set a := CNFrv f2 m => oa. case (equal_or_not (f \0o) \0o)=> ez. rewrite ez oopow0 (osucc_pr oa) => xsa. by move:(oltS oa); rewrite -xsa; move/lx => []; rewrite - xsa. exists a,(f \0c);split => //. case: (equal_or_not m \0c) => mz. by left; rewrite /a mz /CNFrv osum_f0. have cm1: \1c <=c m by apply: cge1; fprops. move : (cdiff_pr cm1) (NS_diff \1c mN); set m' := _ -c _ => mv m'N. set f1' := (fun i => oopow (f2 i)). have oo1:ordinalp (f1' \0c). by apply: OS_oopow;apply:(proj1 ax3); apply/strict_pos_P1. have ha': ord_below f1' (\1c +c m'). move => i il; apply: OS_oopow; apply: (proj1 ax3); ue. have sn0:csucc \0c <c n by rewrite - nv succ_zero;apply:csum_M0lt; fprops. have ez0: f \0c <=o f \1c. by move: (proj2 ax _ NS0 sn0); rewrite succ_zero. have ez': \0o <o f \1c. split; first by move: (ez0) => [_ /ole0x h2 _]. move => b; case ez;rewrite - b in ez0; exact: (ole0 ez0). move:(osum_fA NS1 m'N ha'); rewrite mv -/(CNFrv _ _) -/a. rewrite (osum_f1 oo1); rewrite /f1' /f2 (csum0l CS1) => eq2. have ax4: CNFr_ax (fun z : Set => f ((z +c \1c) +c \1c)) m'. split. move => i im; apply: (proj1 ax3); rewrite - mv (csumC \1c). apply:csum_Mlteq; fprops. move => i iN sim. have eq: (csucc i +c \1c) = csucc (i +c \1c) by rewrite (csum_Sn _ iN). rewrite /f2 eq; apply:(proj2 ax3); first by apply:(NS_sum iN NS1). rewrite - mv (csumC \1c) - eq; apply:csum_Mlteq; fprops. have sa:= (OS_CNFr0 m'N ax4). have sb:= (opow_Mo_le ez0). have la: limit_ordinal a. rewrite eq2;exact:(osum_limit sa (indecomp_limit2 ez')). have le3: omega0 ^o f \0c <=o a. rewrite eq2; apply: (oleT sb); apply: (osum_M0le sa (proj32 sb)). right; split => //. rewrite xv (osum_cardinal oa hc). move: (ocle1 le3) => pc. have pb: omega0 <=o oopow (f \0c). rewrite - oopow1; apply: opow_Mo_le; fprops. move: (ocle1 (oleT pb le3)). rewrite (card_card CS_omega) => pd. by apply: csum_inf => //; apply: (cle_inf_inf CIS_omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)