proposition: Lemma infinite_prod_pC: cprodb Nat \aleph = (\aleph omega0) ^c omega0.
proof: Proof. set x := (Lg Nat \aleph). 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. exact (OS_nat adx). have pb: fg_Mle_lec x. move;rewrite /x; aw; move => a b aB bB ab. rewrite !LgV//;exact (aleph_le_lec ab). rewrite /cprodb (infinite_increasing_power fgf icy pa pb). by rewrite /x (ord_sup_aleph omega_limit); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)