proposition: Lemma infinite_increasing_power5gch X (Y:= Lg (domain X) (fun z => \aleph (Vg X z))) (a := \osup (range X)): ofg_Mlt_lto X -> limit_ordinal (domain X) -> ((cprod Y) = \aleph a ^c (cardinal (domain X)) /\ (cprod Y) = \aleph (osucc a)).
proof: Proof. move => pa pb. move: (infinite_increasing_power5 pa pb). move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe]. have ia:=(CIS_aleph (proj31 pc)). rewrite -/a -/Y. rewrite - (cnextE (proj31 pc)) - (gch ia). move: (cnext_pr1 (proj1 ia)) => [_]. set A := \omega a; set B := A ^c cardinal (domain X). move=> _ qa [qb qc qd]. have qe:= (qa _ qb). have bv := (cleA qc (cleT qd qe)). by split => //; apply:cleA => //; rewrite bv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)