proposition: Lemma cpow_less_ec_pr8 x y ( z := x ^<c y): infinite_c y -> infinite_c x -> [/\ (y <=c \cf x -> z = x), (\cf x <c y -> y <=c cnext x -> z = cnext x) & (cnext x <c y -> z = y)].
proof: Proof. move => icy icx; rewrite /z. have cy:= proj1 icy. have cx:= proj1 icx. have sp1:=(cnext_pr2 cx). have sp1' := proj1 sp1. split. move => pa; move: (cpow_less_pr5a cx (infinite_ge2 icy)) => le1. apply: cleA; last by exact. apply: (card_ub_sup cx) => i /funI_P [t ta ->]; move: ta. move/ (cardinals_ltP cy) => ty. move: (clt_leT ty pa) => lt2. case: (equal_or_not t \0c) => tnz. rewrite tnz cpowx0; apply: (cle_fin_inf finite_1 icx). rewrite (infinite_power10_b icx lt2 tnz); fprops. move => p1 p2; apply: cleA; last first. by move: (cpow_less_pr2 x p1); rewrite (infinite_power10_a icx). apply: (card_ub_sup (proj32 p2)) => i /funI_P [t ta ->]; move: ta. move /(cardinals_ltP cy) => ty. move: (infinite_power10 t icx) => [pa pb pc pd]. case: (equal_or_not t \0c) => tz. rewrite (pa tz); apply: cleT p2. apply: (cle_fin_inf finite_1 icy). case: (cleT_el (proj31_1 p1) (proj31_1 ty)) => ctc. rewrite (pc ctc (cnext_pr4 cx (clt_leT ty p2))); exact:(cleR (proj32 p2)). by rewrite (pb tz ctc). move => qa. apply: cleA. apply: (card_ub_sup cy). move => i /funI_P [t ta ->]; move: ta. move /(cardinals_ltP cy) => ty. move: (infinite_power10 t icx) => [pa pb pc pd]. case: (equal_or_not t \0c) => tz. by rewrite (pa tz); apply: (cle_fin_inf finite_1 icy). move: (cofinality_small icx) => p1. case: (cleT_el (proj31 p1) (proj31_1 ty)) => ctc. case: (cleT_el (proj31_1 ty) cx) => ctx. rewrite (pc ctc ctx); apply: (proj1 qa). rewrite (pd ctx); move: (cnext_pr1 (proj32_1 ctx)). by move => [_ _]; apply. by rewrite (pb tz ctc); apply: (cleT sp1' (proj1 qa)). move: (ord_index_pr1 icy); set c := (ord_index y); move => [qb qc]. move: (ord_index_pr1 icx); set d := (ord_index x); move => [qd qe]. move: (qa); rewrite - {1} qe -qc (cnextE qd) => qa1. move: (aleph_ltc_lt (OS_succ qd) qb qa1) => qa2. case: (ordinal_limA qb) => ln. rewrite ln in qa2;case: (olt0 qa2). move:ln => [e oe se]. move: (cnextE oe); rewrite - se => <-. move: (CIS_aleph oe) => icz. rewrite (cpow_less_pr4 (clt_fin_inf finite_0 icx) icz). move: (infinite_power10 ( \omega e) icx) => [ra rb rc rd]. have xe: x <c \omega e. by rewrite -qe; apply: aleph_lt_ltc; apply /oltSSP; ue. by rewrite (rd xe); apply: cleR; rewrite (cnextE oe) - se qc. rewrite {1} (proj2 (aleph_normal) _ ln). apply: card_ub_sup; first by apply: CS_cpow_less. move => i /funI_P [w wi ->]. have wc: w <o c by apply /oltP. move: (aleph_lt_ltc wc) => le1. apply: cleT (cpow_less_pr2 x le1). apply: (cleT (proj1 (cantor (proj31_1 le1)))). apply: (cpow_Mleeq (\omega w) (infinite_ge2 icx) card2_nz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)