proposition: Lemma infinite_increasing_power5 X (Y:= Lg (domain X)(fun z => \aleph (Vg X z))) (a := \osup (range X)): ofg_Mlt_lto X -> limit_ordinal (domain X) -> [/\ \aleph a <c cprod Y, cprod Y <=c \aleph a ^c cardinal (domain X) & \aleph a ^c cardinal (domain X) <=c \2c ^c \aleph a].
proof: Proof. move => pa pb. move: (infinite_increasing_power4 pa pb) => [qa qb]. move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe]. move: pa => [fgx xo xi]. move: (infinite_increasing_power_bound1 fgx xo); rewrite -/Y -/a => le1. split; [exact | exact |]. move: (cpow_Meqle (aleph_nz (proj31 pc)) qa). rewrite -/a infinite_power1_b //; apply: (CIS_aleph (proj31 pc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)