proposition: Lemma infinite_prod_pI: csumb omega1 (fun z => \aleph z ^c aleph0) = \aleph omega1 ^c aleph0.
proof: Proof. have la: limit_ordinal omega1 by apply: aleph_limit; fprops. have ic: infinite_c omega1 by apply: CIS_aleph; fprops. have cf: omega0 <c cofinality aleph1. move: (proj2 (regular_cardinal_aleph1)). rewrite (cofinality_card ic) => ->. rewrite - aleph0E; apply: aleph_lt_ltc; apply: olt_01. rewrite (infinite_power7f1 la cf) //; first by apply: omega_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)