proposition: Lemma infinite_prod_pH b: ordinalp b -> cprodb omega0 (fun z => (\aleph z) ^c (\aleph b)) = (\aleph omega0) ^c (\aleph b).
proof: Proof. move => ob. have ie := CIS_aleph ob. move/infinite_c_P2 : (ie) => iea. move: (f_equal (fun z => z ^c \aleph b) infinite_prod_pC). rewrite cpow_prod - cpow_pow cprodC (cprod_inf iea ie omega_nz) => <-. by aw; apply: cprodb_exten => x xd; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)