proposition: Lemma infinite_power6_5 a b c : ordinalp a -> ordinalp b -> \aleph (\omega a) = c ^c (\aleph b) -> b <o a.
proof: Proof. move => oa ob. have la:=(aleph_limit oa). have aux: infinite_c (\aleph (\aleph a)). by apply: CIS_aleph; apply: OS_aleph. rewrite -(cpowcl c (\omega b)). set C := cardinal c. case: (equal_or_not C \1c) => eq1. rewrite eq1 cpow1x =>h; move: aux; rewrite h; move: finite_1 => pa pb. case: (finite_not_infinite pa pb). case: (equal_or_not C \0c) => eq0. by rewrite eq0 (cpow0x (aleph_nz ob)) => h;case:(infinite_nz aux). move: (cge2 (CS_cardinal c) eq0 eq1) => c2 h. move: (power_cofinality5 c2 (CIS_aleph ob)). rewrite - (f_equal cofinality h) regular_initial_limit1 //. move: (CIS_aleph oa) => ia. move: (cofinality_small ia) => l1 l2. exact: (aleph_ltc_lt ob oa (clt_leT l2 l1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)