proposition: Lemma infinite_prod5 a: (limit_ordinal a) -> cprodb a \aleph = (\aleph a) ^c (cardinal a).
proof: Proof. move => la. pose p j := limit_ordinal j -> cprodb j \omega = \omega j ^c cardinal j. apply: (least_ordinal2 (p:=p)) (proj31 la) la => y oy etc ly. move: (cantor_of_limit ly) => [c [n [oc on nz yv cp]]]. have np := (ord_ne0_pos on nz). have op:= (OS_pow OS_omega on). case: (equal_or_not c \0o) => cz. move: yv; rewrite cz (osum0l op) => yv. set X := (Lg y id). have dx: domain X = omega0 ^o n by rewrite -yv /X; aw. have osx: ofg_Mlt_lto X. rewrite /X /ofg_Mlt_lto /ordinal_fam;split;fprops. hnf; aw;move => x xy;rewrite LgV//; exact (Os_ordinal oy xy). hnf; aw;move => u v ux vx uv; rewrite !LgV//. move: (infinite_prod3 np osx dx). have ->: (Lg (domain X) (fun z => \omega (Vg X z))) = (Lg y \omega). rewrite /X; aw; apply: Lg_exten => t te; rewrite LgV//. by move => h; rewrite /cprodb h -yv ord_sup_aleph. case: cp => [ cnz // |[lc le1 sv]]. have cy: c <o y. by move: (osum_Meqlt (opow_pos olt_0omega on) oc); rewrite (osum0r oc) -yv. move: (etc _ cy lc); rewrite - sv => eq1. rewrite {1} yv (cprod_An1 \aleph oc op) eq1. set X := Lg (omega0 ^o n) (fun z => (c +o z)). have dx: domain X = omega0 ^o n by rewrite /X; aw. have xx: ofg_Mlt_lto X. split; rewrite /X; fprops. hnf;aw; move => x xv; rewrite LgV//; exact:(OS_sum2 oc (Os_ordinal op xv)). hnf; aw; move => u v ud vd; rewrite !LgV// => lt1. by apply: osum_Meqlt. move: (infinite_prod3 np xx dx); rewrite /cprodb. set L1:= Lg _ _; set L2 := Lg _ _. have ->: L1 = L2 by rewrite /L1 /L2 /X;aw; apply: Lg_exten => x xd; rewrite LgV//. have l1: limit_ordinal (omega0 ^o n) by apply:indecomp_limit2. have ->: union (range L2) = \omega y. move: (normal_ofs_compose aleph_normal (osum_normal oc)) => [_ xb]. by move: (xb _ l1); rewrite -/L2 /= yv; move => ->; rewrite /L2 Lg_range. move => ->;clear L1 L2. have cnz: cardinal y <> \0c. by apply:card_nonempty1; move: ly => [_ ok _]; exists \0c. have le2: cardinal (omega0 ^o n) <=c cardinal y. by apply ocle1; rewrite yv; apply: osum_M0le. by move: (infinite_power5 oc op cnz le2); rewrite -yv => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)