proposition: Lemma infinite_power10 x y (z := x ^c y): infinite_c x -> [/\ (y = \0c -> z = \1c), (y <> \0c -> y <c \cf x -> z = x), (\cf x <=c y -> y <=c x -> z = cnext x)& (x <c y -> z = cnext y)].
proof: Proof. move=> ic; rewrite /z. have x2:= (infinite_ge2 ic). have cx:= proj1 ic. have xx:=(cleR cx). have xnz:= infinite_nz ic. have r1: y = \0c -> x ^c y = \1c by move => ->; rewrite cpowx0. have r2: x <c y -> x ^c y = cnext y. move=> [xy _]. have icy:(infinite_c y) by apply: (cle_inf_inf ic xy). rewrite (gch icy); apply: (infinite_power1_a _ xy icy). apply: cle_fin_inf => //; rewrite /NatP; fprops. move: (cnext_pr1 cx) => [qa qb qc]. have r3: \cf x <=c y -> y <=c x -> x ^c y = cnext x. move=> pa pb. move: (power_cofinality x2); rewrite (cofinality_card ic) => pc. have pd: x ^c (\cf x) <=c x ^c y by apply: cpow_Mlele. have lt1:= (qc _ (clt_leT pc pd)). apply: cleA lt1. rewrite (gch ic) - (infinite_power1_b ic). by apply: cpow_Mlele. split => // ynz ycx. have cy := (proj31_1 ycx). have yl1:=(cge1 cy ynz). apply: cleA; last by apply: cpow_Mle1. rewrite (infinite_power7 ic ycx ynz) /csumb. set f := Lg _ _. have cf: cardinal_fam f by rewrite /f;hnf;aw => a ac;rewrite LgV //; fprops. have fl: forall i, inc i (domain f) -> Vg f i <=c x. rewrite /f; aw; move=> i id; rewrite LgV//. case: (equal_or_not i \0c) => iz. rewrite iz (cpow0x ynz); apply: cle0x; fprops. case: (equal_or_not i \1c) => io. rewrite io (cpow1x); apply: cle_fin_inf => //; apply: finite_1. move: id => /(cardinals_ltP cx) lt. have ci:= proj31_1 lt. case: (Nat_dichot cy) => yN. case: (Nat_dichot ci) => iN. by apply: (cle_fin_inf _ ic); apply /NatP;apply: NS_pow. exact: (cleT (cpow_inf1 iN yN) (proj1 lt)). have ra: forall t, infinite_c t -> t <c x -> \2c ^c t <=c x. move=> t it tx. by rewrite - (gch it); move: (cnext_pr1 (proj1 it))=> [ _ _]; apply. have ray: \2c ^c y <=c x. by apply: ra => //; apply: (clt_leT ycx); apply: cofinality_small. case: (Nat_dichot ci) => iN. have b1:= NS1. have iy: i <=c y by apply (Nat_le_infinite). have i2: \2c <=c i. rewrite - succ_one ; apply /(cleSltP b1). by split; [apply: cge1 | apply:nesym]. rewrite (infinite_power1_a i2 iy yN) //. have i2:= (cle_fin_inf finite_2 iN). case: (cleT_ee ci cy) => cp1. rewrite (infinite_power1_a i2 cp1 yN) //. have le1: i ^c y <=c i ^c i by apply: cpow_Mlele => //; fprops. apply: (cleT le1). rewrite (infinite_power1_b iN); exact: (ra _ iN lt). have df: domain f = (cardinals_lt x) by rewrite /f; aw. move: (infinite_power7d cx xnz)=> [pe pf]. have fgf: fgraph f by rewrite /f; fprops. move: (csum_of_small_b1 (conj fgf fl)). rewrite Lgd - (cprod2cr)(cprod_inf pe ic pf) => aux. by apply cprod_inf4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)