proposition: Lemma cpow_less_ec_pr6 x y: infinite_c y -> \2c <=c x -> ~ (exists a, cpow_less_ec_prop x y a) -> \cf (x ^<c y) = \cf y.
proof: Proof. move => pa pb pc. symmetry. move: (cpow_less_ec_pr5 pa pb pc) => [X [q1 q2 q3 q4 q5]]. have icz: infinite_c (x ^<c y) by apply: cpow_less_ec_pr0. have fgY: fgraph (Lg (domain X) (fun z : Set => x ^c Vg X z)) by fprops. move: (icz) => [[oz _] _]; move: (icz) => [cz _]. apply: cleA; last first. move: q5; set v := range _ => e1. have h: sub v (x ^<c y). move => t /(range_gP fgY);aw; move => [z /q3 h ->]. by move :(oclt h) => /(oltP oz). move: (cofinality_pr8 oz h e1). move: (range_smaller fgY); rewrite -/v q1 Lgd. rewrite (card_card (CS_cofinality (proj1 (proj1 pa)))) => l1 l2. exact: cleT l2 l1. move: (cofinality_pr4 oz). move => [f [[[ff sf tf] cff] fb] fc]. have xnz:= (card_ge2_nz pb). have ra: forall a, a <c y -> exists b, [/\ a <c b, b <c y & x ^c a <c x^c b]. move => a ay; ex_middle bad; case: pc; exists a; split => //. move => b ab lby; ex_middle ne. case: bad; exists b; split => //; split => //; first by dneg eq0; rewrite eq0. exact (cpow_Meqle xnz ab). have rb: forall i, inc i (source f) -> exists t, inc t y /\ cardinal (Vf f i) <=c x ^c t. move => i isf. have /(oltP oz) la: inc (Vf f i) (x ^<c y) by rewrite - tf; Wtac. have ou:= proj31_1 la. move/(ocle2P cz ou): la => lb. move:pa => [cy _]; move: (cy) => [oy _]. move: (clt_sup (@cpow_less_pr0 x y) lb) => [v /funI_P[w]]. move /(cardinals_ltP cy)=> /oclt => rb -> /proj1 rc. by exists w; split => //; apply /(oltP oy). pose g i := choose (fun t => inc t y /\ cardinal (Vf f i) <=c x ^c t). have gp: forall i, inc i (source f) -> inc (g i) y /\ cardinal (Vf f i) <=c x ^c (g i). move => i /rb h; apply: (choose_pr h). move: (fun_image_smaller (source f) g). have oy:=(proj1 (proj1 pa)). set G := fun_image (source f) g; rewrite sf (card_card (CS_cofinality oz)). have sgy: sub G y by move => t /funI_P [z /gp [ h _] ->]. suff ugy: \osup G = y by apply: cleT; exact (cofinality_pr8 oy sgy ugy). have osy: ordinal_set y by move => t/(Os_ordinal oy). have ->: y = union y. by move: (limit_nonsucc (infinite_card_limit2 pa)). apply: (ord_sup_1cofinal) => //; split => // a /(oltP oy) lay. have oa:= proj31_1 lay. move /(ocle2P (proj1 pa) oa): lay => /ra [b [sa sb sc]]. have: inc (x ^c b) (x ^<c y). apply /(oltP oz); move: (ra _ sb) => [b' [b1 b2 b3]]. move: (clt_leT b3 (cpow_less_pr2 x b2)). apply: oclt. rewrite - sf in cff; move /cff => [c c1 /ocle1 c2]. exists (g c); first by apply/funI_P; ex_tac. move/gp: c1 => [sd se]. move: (cleT c2 se); rewrite (card_card (CS_pow x b)) => sg. case: (oleT_ee oa (Os_ordinal oy sd)) => //. move /ocle1 => /(cpow_Meqle xnz); rewrite cpowcr => l3. by move: (clt_leT sc (cleT sg l3)) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)