proposition: Lemma infinite_power6_7e: \aleph omega1 <=c \2c ^c omega0 -> (gimel_fct (\aleph omega0) = \2c ^c aleph0 /\ gimel_fct (\aleph omega1) = \2c ^c aleph1).
proof: Proof. set o1 := \aleph \1o. move => h; rewrite /gimel_fct. have h1: \aleph omega0 <=c \aleph o1. rewrite - aleph0E; apply: aleph_le_lec; apply: (aleph_le_leo ole_01). move: (cleT h1 h) => h2. move: (regular_initial_limit1 (aleph_limit OS0)); rewrite aleph0E. move: (regular_initial_limit1 (aleph_limit OS1)); rewrite -/o1. move => -> ->. have pa:= (CIS_aleph OS_omega). rewrite (proj2 regular_omega). move: (regular_cardinal_aleph1) => [pb]. rewrite (cofinality_card pb) -/o1; move => ->. have cn2:=card2_nz. split. apply: cleA. move: (cpow_Mleeq omega0 h2 (infinite_nz pa)). rewrite - cpow_pow csquare_inf //; apply: CIS_omega. apply: cpow_Mleeq => //; apply: cle_fin_inf => //; fprops. move: (CIS_aleph (proj1 (proj1 pb))); rewrite -/o1 => io1. have aux: (omega0 *c o1) = o1. rewrite cprodC; apply: (cprod_inf _ pb omega_nz). rewrite - aleph0E; exact (aleph_le_lec ole_01). apply: cleA. move: (cpow_Mleeq o1 h (infinite_nz io1)). by rewrite - cpow_pow aux. exact: (cpow_Mleeq _ (infinite_ge2 io1) cn2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)