proposition: Lemma infinite_power6w y: infinite_c y -> ( (exists2 x, y <c x & x ^c y = x) /\ (exists2 x, y <c x & x <c x ^c y)).
proof: Proof. move => h; split. exists (\2c ^c y); first by apply: (cantor (proj1 h)). rewrite - cpow_pow csquare_inf //. move: (ord_index_pr1 h)=> [on yv]. move: (cnextE on); rewrite yv; set z:= cnext y => zv. have yz: y <c z by rewrite -yv zv; apply: aleph_pr10c. have oz:= (OS_cardinal (proj32_1 yz)). have osn:= (OS_succ on). have zp: \aleph z <> z. move=> eq; rewrite {2} zv in eq. move: (aleph_inj oz osn eq). move: (aleph_limit osn); rewrite - zv; move => [la lb lc] zs. have nz: inc (ord_index y) z by rewrite zs /osucc; fprops. move: (lc _ nz); rewrite - zs => bad; exact (ordinal_irreflexive oz bad). have tp:= (normal_ofs_fix aleph_normal oz). have cft:= (cofinality_least_fp_normal aleph_normal zp tp). move: tp =>[]; set t := the_least_fixedpoint_ge _ _ => tp1 tp2 tp3. have cz: cardinalp z by rewrite zv; apply: CS_aleph. have ct: cardinalp t by rewrite -tp2; apply: (CS_aleph (proj32 tp1)). have yt: y <c t. apply: (clt_leT yz). rewrite - (card_card cz) - (card_card ct). by apply: ocle1. have ict: infinite_c t by apply: (cle_inf_inf h (proj1 yt)). exists t => //. apply: (clt_leT (power_cofinality (infinite_ge2 ict))). apply: cpow_Mlele. by apply: infinite_nz. move: ict => [cat _]; fprops. by rewrite (cofinality_card ict) cft; apply /infinite_c_P2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)