proposition: Lemma infinite_power6_7c: \2c ^c aleph1 = aleph2 -> \aleph omega1 <c (\aleph omega0) ^c aleph0 -> \aleph omega1 ^c aleph1 = (\aleph omega0) ^c aleph0.
proof: Proof. set x1 := \aleph omega1. set x2 := \aleph omega0 ^c aleph0. move => pa [pb _]. have pc:= (aleph_nz OS_omega). have x1nz := (aleph_nz (OS_aleph OS1)). move: (aleph_le_lec ole_01); rewrite aleph0E => pd. have pe:= (aleph_le_lec (ocle pd)). have pf := (cpow_Mleeq aleph0 pe pc). symmetry;apply: cleA. apply: (cleT pf); apply: cpow_Meqle => //; apply: aleph_nz. have: x1 ^c \aleph \1o <=c x2 ^c \aleph \1o by apply: cpow_Mleeq. move: (infinite_power6_7a pa); rewrite -/x2 ; move => <-. rewrite - cpow_pow csquare_inf //;apply: CIS_aleph; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)