proposition: Lemma cpow_less_ec_pr7 x y z (p := (x ^<c y) ^c z): infinite_c y -> \2c <=c x -> [/\ ( \1c <=c z -> z <c \cf y -> p = x ^<c y), (\cf y <=c z -> z <c y -> p = x ^c y) & (y <=c z -> p = x ^c z)].
proof: Proof. move => icy x2. have ia:= (cpow_less_ec_pr0 icy x2). have ca := proj1 ia. have aux: forall z, infinite_c z -> \cf z <=c z. move =>t icz;move: (icz) => [cz _]; move:(cz) => [oz _]. apply: ocle3 => //; first by apply: CS_cofinality. by apply: cofinality_pr3. have cfys := (aux _ icy). case: (p_or_not_p (exists a, cpow_less_ec_prop x y a)). move => [a ha]; split. - move=> z1 z2. have znz: z <> \0c by move/cge1P:z1 => [_ /nesym]. have hb:= (cpow_less_ec_pr2 ha x2). have pb:= (clt_leT z2 cfys). have cz := (proj31_1 z2). rewrite /p. case: (finite_or_infinite cz) => fz. have zN: natp z by apply /NatP. by rewrite (cpow_inf ia zN znz). have [b [b1 b2 b3]]: exists b, [/\ a <=c b, z <=c b & b <c y]. move: ha => [ay _]; move: (ay) => [[ca1 _] _ _]. case: (cleT_ee ca1 cz) => le1. by exists z; split => //; apply: cleR. exists a; split;fprops. have ib:=(cle_inf_inf fz b2). by rewrite /p (hb _ b1 b3) - cpow_pow (cprod_inf b2 ib znz). - move => pa pb. have sy: singular_cardinal y. by split => //; move: (cle_ltT pa pb) => [_]. move: (cpow_less_ec_pr3 ha x2 sy) => [pc pd]. rewrite /p pd - cpow_pow (cprod_inf (proj1 pb) icy) //. move: (cofinality_infinite_cardinal icy) => i1. exact: (infinite_nz (cle_inf_inf i1 pa)). - move => yz. move: (cpow_less_ec_pr2 ha x2) => hb. move: ha => [ay _];move: (ay) => [[oa _] _ _]. case: (equal_or_not a \0c) => az. have y1: \1c <c y by apply: (clt_fin_inf finite_1 icy). move: cle_01; rewrite - az => ab. rewrite /p (hb _ ab y1) (cpowx1 (proj32 x2)) //. rewrite /p (hb _ (cleR oa) ay) - cpow_pow (cprodC). have iz:= (cle_inf_inf icy yz). by rewrite (cprod_inf (cleT (proj1 ay) yz) iz az). move => ha. have hb:= (cpow_less_ec_pr6 icy x2 ha). move: (cpow_less_ec_pr5 icy x2 ha) => [X]. set Y := Lg (domain X) (fun z0 : Set => x ^c Vg X z0). move => [q1 q2 q3 q4 q5]. have fgY: fgraph Y by rewrite /Y; fprops. have q6: cardinal_fam Y by rewrite /Y; hnf;aw;move => t td; rewrite LgV//; fprops. have q10: csum Y = x ^<c y. have pa: infinite_c (union (range Y)) by rewrite q5. have pb: cardinal (domain Y) <=c union (range Y). rewrite q5 in pa. have pb := aux _ pa. by rewrite q5 /Y; aw; rewrite q1 -hb (card_card (proj31 pb)). by rewrite (csum_of_small_b4 fgY q6 pa pb) q5. have xx: \1c <=c z -> z <c \cf y -> p = x ^<c y. move => z1 zcy. rewrite -hb in zcy. have znz: z <> \0c by move/cge1P:z1 => [_ /nesym]. rewrite /p (infinite_power7 ia zcy znz) /csumb. set T := Lg _ _. have pa: (forall i, inc i (domain T) -> Vg T i <=c x ^<c y). rewrite /T; aw => i id; rewrite LgV//. move: id => /(cardinals_ltP ca) => le2. have csr: cardinal_set (range Y). by move => t /(range_gP fgY) [w wi ->]; apply: q6. move: le2; rewrite - {1} q5 => le2. move: (clt_sup csr le2); move => [v ]. move /(range_gP fgY); rewrite /Y;aw; move => [w wdx ->];rewrite LgV// => /proj1 le3. case: (equal_or_not i \0c) => iz. rewrite iz (cpow0x znz); apply: (cle0x ca). move: (cpow_Mleeq z le3 iz); rewrite - (cpow_pow) => pb. apply (cleT pb); apply: (cpow_less_pr2). move: (q2 _ wdx) => le1. rewrite hb in zcy; move: (clt_leT zcy cfys) => le4. by apply: cprod_inf5. have ct: cardinal_fam T by rewrite /T; hnf;aw; move => a ad;rewrite LgV; fprops. have ct': fgraph T by rewrite /T; fprops. have dt: domain T = cardinals_lt (x ^<c y) by rewrite /T; aw. move: (csum_of_small_b1 (conj ct' pa)). rewrite dt - cprod2cr. move: (infinite_power7d ca (infinite_nz ia)). set t := cardinal _; move=> [le2 tnz]. have snz: csum T <> \0c. have zt: inc \1c (domain T). rewrite /T;aw; apply /(cardinals_ltP ca). apply: (clt_fin_inf finite_1 ia). move: (csum_increasing6 (ct _ zt) zt). move: zt; rewrite {1}/T; aw => zt;rewrite {1} /T; rewrite LgV//. by rewrite cpow1x; move/cge1P => [_ /nesym]. rewrite (cprod_inf le2 ia tnz) => le3. by rewrite cprodC (cprod_inf le3 ia snz). case: (equal_or_not y omega0) => yo. split => //. by move:regular_omega => [ra rb];rewrite yo rb => l1 /(cleNgt l1). move => yz;rewrite /p yo. have oic:= CIS_omega. have o2:=(cle_fin_inf finite_2 oic). rewrite yo in yz. have icz: infinite_c z by apply: (cle_inf_inf oic yz). case: (finite_or_infinite (proj32 x2)) => fx. rewrite (cpow_less_pr5c x2 fx). rewrite (infinite_power1_a o2 yz icz). by rewrite (infinite_power1_a x2 (cle_fin_inf fx icz) icz). by rewrite (cpow_less_pr5e fx). have xnz:= (card_ge2_nz x2). have pa: forall z, infinite_c z -> (x ^<c y) ^c z <=c x ^c (csum (Lg (domain X) (fun t => (Vg X t) *c z))). move => w wi; rewrite - q10. have pb: (forall i, inc i (domain Y) -> \2c <=c Vg Y i). rewrite /Y; aw => i idx; rewrite LgV//. move: (q4 yo _ idx) => enz. exact: (cleT x2 (cpow_Mle1 (proj32 x2) enz)). have le1 := (compare_sum_prod1 fgY pb). have le0: csum Y <> \0c by rewrite q10; apply: infinite_nz. apply: (cleT (cpow_Mleeq w le1 le0)). rewrite (cpow_prod _ Y) cpow_sum /Y. rewrite /cprodb. rewrite !Lgd; set f1 := Lg _ _; set f2 := Lg _ _. have ->: f1 = f2 by apply: Lg_exten => t te; rewrite !LgV// - cpow_pow. apply: cleR; rewrite /cprod; fprops. move: (cofinality_infinite_cardinal icy) => cyi. split => //. move => p1 p2. have icz: (infinite_c z) by apply: (cle_inf_inf cyi p1). move: (pa _ icz); set f := Lg _ _ => pb. have pc: csum f <=c y. have df: domain f = \cf y by rewrite /f; aw; ue. have cf0: fgraph f by rewrite /f; fprops. have cf2: (forall i, inc i (domain f) -> Vg f i <=c y). rewrite /f; aw => i idx; rewrite LgV//; rewrite cprodC. apply: (cprod_inf4 (proj1 p2) (proj1 (q2 _ idx)) icy). move: (csum_of_small_b1 (conj cf0 cf2)). by rewrite df (cprod_inf cfys icy (infinite_nz cyi)). apply:cleA; first by apply: (cleT pb (cpow_Meqle xnz pc)). rewrite /p (cpow_less_pr6 icy x2); apply: (cpow_Meqle (infinite_nz ia) p1). move => p1. have icz: (infinite_c z) by apply: (cle_inf_inf icy p1). move: (pa _ icz); set f := Lg _ _ => p2. have pb: x ^c csum f <=c x ^c z. apply: (cpow_Meqle xnz). have cf1: fgraph f by rewrite /f; fprops. have cf2: (forall i, inc i (domain f) -> Vg f i <=c z). rewrite /f; aw => i idx; rewrite LgV//; rewrite cprodC. apply: cprod_inf1 => //. exact (cleT (proj1 (q2 _ idx)) p1). have df: domain f = \cf y by rewrite /f; aw; ue. move: (csum_of_small_b1 (conj cf1 cf2))=> l3; apply:(cleT l3). rewrite df; exact: (cprod_inf1 (cleT cfys p1) icz). apply: (cleA (cleT p2 pb)). exact: (cpow_Mleeq z (cpow_less_pr5a (proj32 x2) (infinite_ge2 icy)) xnz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)