proposition: Lemma infinite_prod_pD (o2 := omega0 +o omega0): cprodb o2 \aleph = (\aleph o2) ^c omega0.
proof: Proof. set oo := (\aleph o2). move: OS_omega => ioo. apply: cleA. have -> : oo ^c omega0 = oo ^c (omega0 +o omega0). by rewrite - cpowcr cardinal_omega2 cpowcr. have oo2: ordinalp o2 by apply: OS_sum2. rewrite - cprod_of_same /cst_graph; apply: cprod_increasing; aww. by move=> x xB; rewrite !LgV//; apply: aleph_le_lec; apply/(oleP oo2); apply:setU1_r. set p1:= cprod (Lg omega0 (fun z => (\aleph (omega0 +o z)))). set x := (Lg omega0 (fun z : Set => \aleph (omega0 +o z))). have fgf: fgraph x by rewrite / x; fprops. have icy: infinite_c (domain x) by rewrite /x; aw; apply: CIS_omega. have pa: cardinal_pos_fam x. move;rewrite /x; aw; move=> a adx; rewrite /x LgV//; apply: aleph_nz1. by apply: OS_sum2 => //; apply(Os_ordinal ioo adx). have pb: fg_Mle_lec x. move;rewrite /x; aw; move => a b aB bB ab; rewrite !LgV//. exact (aleph_le_lec (osum_Meqle ab ioo)). move: (infinite_increasing_power fgf icy pa pb). have ->: union (range x) = oo by apply: (ord_sup_aleph_sum ioo). rewrite {2} /x; aw; move => <-. move: (cprod_An1 \aleph ioo ioo) => ->. have fg1: fgraph (Lg omega0 \aleph) by fprops. rewrite cprodC; apply: cprod_M1le; rewrite /cprod;fprops. apply /cprod_nzP; hnf;aw => i id; rewrite LgV//; apply:(aleph_nz(Os_ordinal ioo id)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)