proposition: Lemma infinite_power9 x y: infinite_c x -> infinite_c y -> [/\ (x <=c y -> x ^c y = \2c ^c y), (forall z, z <c x -> x <=c z ^c y -> x ^c y = z ^c y) & ((forall z, z <c x -> z ^c y <c x) -> ( ( y <c \cf x -> x ^c y = x) /\ (\cf x <=c y -> x ^c y = x ^c (\cf x))))].
proof: Proof. move => icx icy. have ynz:=(infinite_nz icy). have xnz:= (infinite_nz icx). split. by move => h; apply: infinite_power1_a => //; apply: infinite_ge2. move=> z le1 le2; apply: cleA. rewrite - {2} (csquare_inf icy) cpow_pow. by apply: cpow_Mleeq. have znz: z <> \0c. move=> bad; case: xnz; move: le2; rewrite bad cpow0x // => b1. apply (cle0 b1). apply: cpow_Mleeq => //; exact (proj1 le1). move => h. have x2: \2c <c x by apply: clt_fin_inf => //; apply /NatP; fprops. have yx:= (cle_ltT (proj1 (cantor (proj1 icy))) (h _ x2)). have [on xv]:= (ord_index_pr1 icx). case: (ordinal_limA on) => nz. move: yx; have ->: x = omega0 by rewrite -xv nz aleph0E. by move: icy => /infinite_c_P2 icy /(cleNgt icy). move:nz=> [m om nv]. move: (regular_initial_successor om) => /regular_cardinalP [_ ww]. move: yx h; rewrite -xv nv ww => yo h;split; last by move=> /(cltNge yo). have le2 := (h _ (aleph_pr10c om)). move => _. move: (infinite_power2 om ynz). have pa: (infinite_c (\aleph (osucc m))) by apply: CIS_aleph; ue. have pb:=(cpow_nz (b := y) (aleph_nz om)). by rewrite cprodC (cprod_inf (proj1 le2) pa pb). split. rewrite -xv (regular_initial_limit1 nz) => yc. move: (infinite_power7e nz ynz). rewrite (infinite_power7f nz yc). set T := fun_image _ _; move=> le1. apply: cleA => //. apply: (card_ub_sup (proj31 le1)). move => a /funI_P [z zn ->]; rewrite - xv in h. have aux : \aleph z <c \aleph (ord_index x). by apply: aleph_lt_ltc; move: zn =>/oltP []. apply: (proj1 (h _ aux)). rewrite -xv; move=> cf1. have oxne: \aleph (ord_index x) <> \0c by ue. apply: cleA; last by apply: cpow_Meqle. rewrite {1} (infinite_power8 on cf1); set T2:= fun_image _ _. case: (equal_or_not (union T2) \0c) => unz. rewrite unz cpow0x; first by apply: cle0x; fprops. apply: infinite_nz; apply:cofinality_infinite_cardinal; ue. apply: cpow_Mleeq => //. apply: card_ub_sup; first by rewrite xv; exact (proj1 icx). move=> a; rewrite /T2 xv => /funI_P [z zi ->]. move: zi => /(cardinals_ltP (proj1 icx)) zi. exact: (proj1 (h _ zi)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)