Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset14.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Ordinals5.

Lemma infinite_power1 a b: \2c <=c a -> a <=c (\2c ^c b) -> infinite_c b ->
   a ^c b = \2c ^c b.
Proof.
move=> le1 le2 ic.
have bb: b <=c b by move: ic => [cb _]; fprops.
have ap: a <> \0c.
  move => h; rewrite h in le1; move: card_lt_02 => lt1; co_tac.
move: card2_nz => tz.
move: (cpow_Mlele ap le2 bb)(cpow_Mlele tz le1 bb).
rewrite - cpow_pow (square_of_infinite ic).
apply: card_leA.
Qed.

Lemma infinite_power1_a a b: \2c <=c a -> a <=c b -> infinite_c b ->
   a ^c b = \2c ^c b.
Proof.
move => pa pb pc; apply: infinite_power1 => //.
move: (cantor (proj1 pc)) => [le1 _]; co_tac.
Qed.

Lemma infinite_power1_b x: infinite_c x -> x ^c x = \2c ^c x.
Proof.
move => ix; apply: infinite_power1_a => //.
  apply: finite_le_infinite => //; apply /BnatP; fprops.
move: ix => [cx _]; fprops.
Qed.

Lemma infinite_power1_c x: infinite_c x ->
  (succ_c x) ^c x = \2c ^c x.
Proof.
move=> ix; move:(ix) =>[cx _].
apply: infinite_power1 => //; last by apply: (succ_c_pr3 cx).
apply: (card_leT (finite_le_infinite finite_2 ix) (proj1 ((succ_c_pr2 cx)))).
Qed.

Section Exercise3_3.
Variables f g :Set.
Hypothesis (fgf: fgraph f)(fgg: fgraph g).
Hypothesis sd: domain f = domain g.
Hypothesis hg: (forall i, inc i (domain g) -> \2c <=c (Vg g i)).

Lemma compare_sum_prod1:
   (card_sum g) <=c (card_prod g).
Proof.
case: (emptyset_dichot (domain g)) => dge.
  rewrite csum_trivial // cprod_trivial //; fprops.
move: dge => [i idg].
case: (equal_or_not (domain g) (singleton i)) => dgs.
  have c1: cardinalp (Vg g i) by move: (hg idg) => [_ le1 _].
  rewrite (csum_trivial1 dgs c1) (cprod_trivial1 dgs c1).
  fprops.
pose h j := choose (fun z => [/\ (inc (P z) (Vg g j)), (inc (Q z) (Vg g j))
     & P z <> Q z]).
have gp: forall j, inc j (domain g) ->
   [/\ inc (P (h j)) (Vg g j), (inc (Q (h j)) (Vg g j)) & P (h j) <> Q (h j)].
  move=> j jdf; apply choose_pr.
  move: (hg jdf) => aux.
  have aux1: \2c <=c (cardinal (Vg g j)).
    by rewrite card_card => //; move: aux => [_ ok _].
  move: aux1 => /card_le2P [a [b [ae be ab]]].
  exists (J a b); aw;split => //.
rewrite /card_prod /card_sum.
set Pr := (productb g); set (Sr := (disjointU g)).
suff [h2 [hp6 hp8]]: exists h2,
  ( (forall j x, inc j (domain g) -> inc x (Vg g j) -> inc (h2 j x) Pr)
  /\ (forall j k x y, inc j (domain g) ->inc k (domain g) ->
    h2 j x = h2 k y -> (x = y /\ j = k))).
  set hh:= Lf (fun z => h2 (Q z) (P z)) (disjointU g) (productb g).
  rewrite /Sr /Pr.
  have ->: (disjointU g) = source hh by rewrite /hh; aw.
  have ->: (productb g) = target hh by rewrite /hh; aw.
  apply: incr_fun_morph; apply: lf_injective.
    by move=> z zf; move: (disjointU_hi zf) => [p1 p2 p3]; apply: hp6.
  move=> u v ud vd; move: (disjointU_hi ud) => [p1 p2 p3].
  move: (disjointU_hi vd) => [p4 p5 p6] eq.
  by move: (hp8 _ _ _ _ p1 p4 eq) => [sp sq]; apply: pair_exten.
have [k1 kdf1 ki1]: exists2 k, inc k (domain g) & k <> i.
  ex_middle ne; case: dgs; set_extens t.
    move=> tdf; apply /set1_P; ex_middle ti; case: ne; ex_tac.
    by move /set1_P => ->.
case: (p_or_not_p (exists k2, [/\ inc k2 (domain g), k2 <> i & k2 <> k1])).
   move=> [k2 [k2df k2i k12]].
  pose hh j x:= Lg (domain g) (fun z => Yo (z = j) x (P (h z))).
  have hp1: forall j x, inc j (domain g) -> inc x (Vg g j) -> inc (hh j x) Pr.
    move => j x jdf xv; apply /setXb_P;rewrite /hh;bw;split;fprops.
    by move => z zdf; bw; Ytac zj; [ ue |move: (gp _ zdf) => [] ].
  have hp2: forall j x y, inc j (domain g) -> (hh j x = hh j y) -> x = y.
    by move=> j x y jdf sh;move:(f_equal (Vg^~j) sh);rewrite/hh; bw;Ytac0;Ytac0.
  have hp3: forall j k x y, inc j (domain g) -> inc k (domain g)-> j <> k ->
     (hh j x = hh k y) -> (x = P (h j) /\ y = P (h k)).
    move=> j l x y jdf ldf jl sh;split.
      by move: (f_equal (Vg^~ j) sh); rewrite /hh; bw; Ytac0; Ytac0.
    by move: (f_equal (Vg^~ l) sh); rewrite /hh; bw; Ytac0; Ytac0.
  pose h1 j := Lg (domain g) (fun z : Set => Yo (z = j) (P (h z)) (Q (h z))).
  have hp4: forall j, inc j (domain g) -> inc (h1 j) Pr.
    move => j jdf; apply /setXb_P;rewrite /h1;bw;split;fprops.
    by move=> z zdf; bw; move:(gp _ zdf) => [za zb _]; Ytac zj.
  have hp5: forall j j', inc j (domain g) -> (h1 j = h1 j') -> j = j'.
    move=> j j' jdf sh;ex_middle jj'; move: (f_equal (Vg ^~j) sh).
    rewrite /h1; bw;Ytac0; Ytac0.
    by move:(gp _ jdf) => [_ _ zc].
  pose h2 j x := Yo (x = P (h j)) (h1 j) (hh j x).
  exists h2; split.
    move=> j x jdf xV; rewrite /h2; Ytac e1; [by apply: hp4 | by apply: hp1].
  have hp7: forall j k x, inc j (domain g) ->inc k (domain g) ->
     hh j x <> h1 k.
    move=> j k x jdf kdf; rewrite /hh /h1; bw.
    suff [z [zdf z1 z2]]: (exists z, [/\ inc z (domain g), z <> j & z <> k]).
      move=> eq; move: (f_equal (Vg ^~z) eq); bw; Ytac0; Ytac0.
      by move: (gp _ zdf) => [_ _].
    case: (equal_or_not j i) => ji.
      case: (equal_or_not k k1) => kk1.
        exists k2; rewrite ji kk1;split => //.
        by exists k1; rewrite ji;split => //; apply: nesym.
    case: (equal_or_not k i) => kk1; last by exists i; split => //;apply: nesym.
    case: (equal_or_not j k1) => jk2.
     by exists k2; rewrite kk1 jk2.
   by exists k1; rewrite kk1; split => //; apply: nesym.
  move=> j k x y jdf kdf; rewrite /h2; Ytac e1.
    Ytac e2.
      by move=> sh1; move: (hp5 _ _ jdf sh1) => aux; rewrite e1 e2 aux.
    by move => aux; case: (hp7 _ _ y kdf jdf).
  Ytac e2 => sh1; first by case: (hp7 _ _ x jdf kdf).
  case: (equal_or_not j k) => e3.
     split => //;rewrite e3 in sh1; apply: (hp2 _ _ _ kdf sh1).
  by move: (hp3 _ _ _ _ jdf kdf e3 sh1) => [aux1 aux2].
move=> aux.
have dfp: forall j, inc j (domain g) -> j = i \/ j = k1.
  move=> j jdf; case: (equal_or_not j i); first by left.
  case: (equal_or_not j k1); first by right.
  move=> jk1 ji; case: aux; exists j;split => //.
clear aux.
move: (gp _ idg) (gp _ kdf1).
set a1:= (P _); set a2 := (Q _);set b1:= (P _); set b2 := (Q _).
move=> [a1v a2v a12] [b1v b2v b12].
pose F x y := Lg (domain g) (fun z => (Yo (z = i) x y)).
have fP: forall x y, inc x (Vg g i) -> inc y (Vg g k1) -> inc (F x y) Pr.
  move=> x y xv yx; apply /setXb_P; rewrite /F /Pr; split;fprops; bw.
  move=> j jdf; bw; Ytac jv; try ue.
  case: (dfp _ jdf) => // -> //.
pose h2 j x := Yo (j = i) (Yo (x = a1) (F a1 b1)
             (Yo (x = a2) (F a2 b1) (F x b1)))
        (Yo (x = b1) (F a1 b2)
        (Yo (x = b2) (F a2 b2) (F a1 x))).
exists h2; split.
  move => j x jdf xv; rewrite /h2; Ytac ji.
    Ytac xa1; [ by apply: fP | Ytac xa2; [ by apply: fP |apply: fP => //; ue]].
  Ytac xb1; [ by apply: fP | Ytac xb2; [ by apply: fP| apply: fP => //]].
  by case: (dfp _ jdf) => //; move=> <-.
have Fi1: forall x y x' y', F x y = F x' y' -> x = x'.
  by move=> x y x' y' eq;move:(f_equal (Vg^~i) eq); rewrite /F; bw;Ytac0; Ytac0.
have Fi2: forall x y x' y', F x y = F x' y' -> y = y'.
  by move=> x y x' y' eq;move:(f_equal (Vg^~k1) eq);rewrite /F; bw;Ytac0; Ytac0.
move=> j k x y jdf kdf; rewrite /h2; bw.
Ytac ij.
  Ytac xa1.
    Ytac ki.
      Ytac ya1; first by rewrite ij ki xa1 ya1//.
      Ytac ya2; move=> eq; move:(Fi1 _ _ _ _ eq) ; first by done.
      by move => eql; case: ya1; rewrite eql.
    Ytac yb1; first by move=> eq; move: (Fi2 _ _ _ _ eq).
    Ytac yb2; move=> eq; move: (Fi2 _ _ _ _ eq); first done.
    by move => eql; case: yb1; rewrite eql.
  Ytac xa2.
    Ytac ki.
      Ytac ya1; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
      Ytac ya2; first by rewrite ij ki xa2 ya2//.
      by move=> eq; move:(Fi1 _ _ _ _ eq)=> eql; case: ya2; rewrite eql.
      Ytac yb1; first by move=> eq; move: (Fi2 _ _ _ _ eq).
     Ytac yb2; move=> eq; move: (Fi2 _ _ _ _ eq); first by done.
     by move => eql; case: yb1; rewrite eql.
  Ytac ki.
    Ytac ya1; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
    Ytac ya2; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
    move=> eq; move:(Fi1 _ _ _ _ eq) => eql; rewrite ij ki; split => //.
  Ytac yb1; first by move=> eq; move: (Fi2 _ _ _ _ eq).
  Ytac yb2; move=> eq; move: (Fi2 _ _ _ _ eq); first by done.
  by move => eql; case: yb1; rewrite eql.
case: (dfp _ jdf) => // jk1.
Ytac xb1.
  Ytac ki.
    Ytac ya1; first by move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: b12.
    Ytac ya2; by move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: b12.
  case: (dfp _ kdf) => // kk1.
  Ytac yb1; first by rewrite jk1 kk1 xb1 yb1; split => //.
  Ytac yb2; first by move=> eq; move: (Fi1 _ _ _ _ eq).
  by move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: yb2.
Ytac xb2.
  Ytac ki.
    by Ytac ya1; [| Ytac ya2 ];
      move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: b12.
  Ytac yb1; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
  case: (dfp _ kdf) => // kk1.
  Ytac yb2; first by rewrite jk1 kk1 xb2 yb2; split => //.
  by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
Ytac ki.
  by Ytac ya1; [| Ytac ya2 ]; move=> eq;move:(Fi2 _ _ _ _ eq) => eql; case: xb1.
rewrite jk1;case: (dfp _ kdf) => // -> aux; split => //; move: aux.
Ytac yb1; [ | Ytac yb2 ];move=> eq; move: (Fi2 _ _ _ _ eq) => //.
Qed.

Lemma compare_sum_prod2:
  (forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)) ->
  (card_sum f) <=c (card_prod g).
Proof.
move=> ale1.
move: (csum_increasing sd ale1) => le1.
move: (compare_sum_prod1)=> le2; co_tac.
Qed.

Lemma compare_sum_prod3:
  (forall i, inc i (domain f) -> (Vg f i) <c (Vg g i)) ->
  (card_sum f) <c (card_prod g).
Proof.
move=> alt1.
have ale1: (forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)).
  by move => i idf; move: (alt1 _ idf) => [ok _].
split; first by apply: compare_sum_prod2.
move /card_eqP=> [h [bh sh th]].
pose D i := (Vg f i) *s1 i.
have Dp1: forall i, inc i (domain f) -> sub (D i) (source h).
  move=> i idf t td. rewrite sh; apply /setUb_P.
  rewrite /disjointU_fam; bw; ex_tac; bw.
pose A i := image_by_fun h (D i).
have Dp2: forall i, inc i (domain f) -> (cardinal (A i)) <c (Vg g i).
  move: (bh) => [ih _].
  move=> i idf;move: (equipotent_restriction1 (Dp1 _ idf) ih).
  move /card_eqP; rewrite -/ (A i).
  have: cardinal (D i) = cardinal (Vg f i).
     apply /card_eqP; rewrite /D; eqsym; fprops.
  move: (alt1 _ idf) => aux.
  have cv: cardinalp (Vg f i) by co_tac.
  by rewrite (card_card cv) => -> <-.
have fh: function h by fct_tac.
have Dp3: forall i, inc i (domain f) -> sub (A i) (target h).
  by move=> i idf; apply: fun_image_Starget1.
have Dp4: forall i F, inc i (domain f) -> sub F (target h) ->
  (cardinal (image_by_fun (pr_i g i) F)) <=c (cardinal F).
  rewrite th; move=> i F idf Fp; apply: surjective_cardinal_le.
  have idg: inc i (domain g) by ue.
  exists (restriction1 (pr_i g i) F); split => //; rewrite /restriction1; aw.
  apply: restriction1_fs; first by apply: pri_f => //.
  rewrite /pr_i; aw.
have Dp5: forall i, inc i (domain f) ->
  (cardinal (image_by_fun (pr_i g i) (A i))) <c (Vg g i).
  move=> i idf; move: (Dp2 _ idf) (Dp4 _ _ idf (Dp3 _ idf)) => le1 le2; co_tac.
have Dp6: forall i, inc i (domain f) -> exists xi, inc xi (Vg g i) /\
    (forall y, inc y (A i) -> Vf (pr_i g i) y <> xi).
  move=> i idf; move: (Dp5 _ idf); set T := image_by_fun _ _.
  have fp: function (pr_i g i) by apply: pri_f => //; ue.
  have st: sub T (Vg g i).
    by move: (@fun_image_Starget1 _ fp (A i)); rewrite {2} /pr_i lf_target.
  have cv: cardinalp (Vg g i) by move: (alt1 _ idf) => lt1;co_tac.
  rewrite -{1} (card_card cv); move=> [_ neq].
  ex_middle nex; case: neq;apply:f_equal; apply:extensionality =>//.
  have sAi: sub (A i) (source (pr_i g i)).
    by rewrite /pr_i; aw; rewrite -th; apply: Dp3.
  move=> x xv; apply /(Vf_image_P fp sAi).
  ex_middle ney; case: nex; exists x; split => //.
  move=> y yA;case: (equal_or_not (Vf (pr_i g i) y) x) => //.
  move=> wy; case: ney; ex_tac.
pose k i:= choose (fun xi => inc xi (Vg g i) /\
          (forall y : Set, inc y (A i) -> Vf (pr_i g i) y <> xi)).
have kp: forall i, inc i (domain f) ->
   (inc (k i) (Vg g i) /\ (forall y, inc y (A i) -> Vf (pr_i g i) y <> (k i))).
  move=> i idf; apply choose_pr; apply: (Dp6 _ idf).
set x := Lg (domain g) k.
have xth: inc x (target h).
    rewrite th /x; apply /setXb_P; split;fprops; bw; move=> i idg; bw.
    by rewrite - sd in idg; move: (kp _ idg) => [p1 _].
move: bh => [ih sjh]; move: ((proj2 sjh) _ xth) => [y ysg Wy].
move: ysg; rewrite sh; move /setUb_P.
rewrite/disjointU_fam; bw.
move=> [i idf]; bw => yd.
have xA: inc x (A i).
  by rewrite /A -Wy; apply /(Vf_image_P (proj1 ih)(Dp1 _ idf)); exists y.
move: (kp _ idf) => [_ p2]; move: (p2 _ xA).
rewrite sd in idf; rewrite th in xth.
by rewrite pri_V // /x; bw.
Qed.

End Exercise3_3.

Lemma compare_sum_prod f g:
  fgraph f -> fgraph g -> domain f = domain g ->
  (forall i, inc i (domain f) -> (Vg f i) <c (Vg g i)) ->
  (card_sum f) <c (card_prod g).
Proof.
move=> fgf fgg sd ale1.
set K:= Zo (domain f) (fun i => \2c <=c (Vg g i)).
have kdf: sub K (domain f) by apply: Zo_S.
have kdg: sub K (domain g) by ue.
have aux: forall i, inc i ((domain f) -s K) ->
  (Vg f i = \0c /\ Vg g i = \1c).
  move=> i => /setC_P [idf] /Zo_P aux.
  move: (ale1 _ idf) => le1.
  have cv: cardinalp (Vg g i) by co_tac.
  case: (card_le_to_el CS2 cv); first by move=> h; case: aux;split => //.
  rewrite - succ_one ; move /(card_lt_succ_leP BS1) => h1.
  move: (card_lt1 (card_lt_leT le1 h1)) => p1.
  split; first by apply: p1; co_tac.
  move: le1; rewrite p1; move/card_ge1P => le1.
  co_tac.
have pf:(forall i, inc i ((domain f) -s K) -> Vg f i = \0c).
   by move=> i ic; move: (aux _ ic) => [].
have pg:(forall i, inc i ((domain g) -s K) -> Vg g i = \1c).
  by rewrite - sd;move=> i ic; move: (aux _ ic) => [].
rewrite (csum_zero_unit kdf pf) (cprod_one_unit kdg pg).
apply: compare_sum_prod3; bw.
  by move=> i iK; bw; move: iK => /Zo_P //; case.
by move=> i iK; bw; apply: ale1; apply: kdf.
Qed.

Lemma exists_ordering X: cardinal_fam X ->
   exists f,
   [/\ bijection f, ordinalp (source f), target f = domain X &
     fg_Mle_lec (X \cf (graph f))].
Proof.
move => pb.
set d := domain X.
have [w wp]: exists t, ~(inc t d).
  ex_middle h.
  set z := Zo d (fun z => ~ (inc z z)).
  case: (p_or_not_p (inc z z)) => h2.
    by move: (h2) => /Zo_hi bad.
  by case: (h2); apply: Zo_i => //; ex_middle h1; case: h; exists z.
pose lev Y:= choose(fun z => inc z Y /\ forall u, inc u Y -> Vg X z <=c Vg X u).
have lep: forall Y, sub Y d -> nonempty Y ->
  (inc (lev Y) Y /\ forall u, inc u Y -> Vg X (lev Y) <=c Vg X u).
  move => Y yd [y yY]; apply choose_pr.
  set Z := fun_image Y (Vg X).
  have neZ: nonempty Z by exists (Vg X y); apply /funI_P; exists y.
  have cz: cardinal_set Z.
    by move => t /funI_P [z zy ->]; apply: pb; apply: yd.
  move: (wordering_cardinal_le_pr cz)=> [ [qb qc] qa].
  have qd: sub Z (substrate (graph_on cardinal_le Z)) by rewrite qa; fprops.
  rewrite qa in qc; move: (qc _ (@sub_refl Z) neZ) => [z []].
  rewrite iorder_sr //; move/funI_P => [t ty ->] tmin; exists t; split => //.
  move => u uy.
  have h1: inc (Vg X u) (fun_image Y (Vg X)) by apply/funI_P ; ex_tac.
  by move: (iorder_gle1 (tmin _ h1)); move /graph_on_P1=> [_ _ ok].
pose lew Y:= Yo (nonempty (d -s Y)) (lev (d -s Y)) w.
have lewe: forall Y, nonempty (d -s Y) ->
  (inc (lew Y) (complement d Y) /\
    (forall u : Set, inc u (d -s Y) -> Vg X (lew Y) <=c Vg X u)).
  by move => y ye; rewrite /lew; Ytac0; apply: lep => //; apply: sub_setC.
have lewb: forall Y, inc (lew Y) (d +s1 w).
  move => Y; case: (p_or_not_p (nonempty (d -s Y))) => h.
   move: (lewe _ h) => [] /setC_P [ok _] _; fprops.
  rewrite /lew; Ytac0; fprops.
move: (cantor (CS_cardinal d)); set a := _ ^c _ => lt1.
move: (lt1) =>[[_ ca _] _]; move: (ca) => [oa _].
move: (ordinal_o_wor oa); set r := ordinal_o _ => wor.
have sr: substrate r = a by rewrite /r ordinal_o_sr.
pose lef f := lew (image_of_fun f).
have ts: (forall f, function f -> segmentp r (source f) ->
      sub (target f) (d +s1 w)-> inc (lef f) (d +s1 w)).
  move=> f ff srf sta; apply: lewb.
move: (transfinite_defined_pr lef wor); rewrite /transfinite_def sr.
move: (transfinite_definition_stable wor ts).
set f := transfinite_defined _ _; move=> stf [sjf sf fv].
have ff: function f by fct_tac.
have fi: forall i, inc i a -> Vf f i <> w ->
  forall j, inc j i -> Vf f i <> Vf f j.
  move => i ia fw; move: (fv _ ia); rewrite /lef.
  set E := (image_of_fun (restriction_to_segment r i f)) => eq1.
  move: eq1; case: (p_or_not_p (nonempty (d -s E))) => nt;
      last by rewrite /lew; Ytac0.
  move: (lewe _ nt) => [] /setC_P [_ s1] _ eq; move => j ji sv.
  case: s1; rewrite -eq sv /E.
  have sr1 : (source (restriction_to_segment r i f)) = i.
    rewrite /restriction_to_segment /restriction1; aw.
    rewrite /r ordinal_segment //.
  have sa1: sub (segment r i) (source f) by rewrite sf - sr ;apply: sub_segment.
  have ji1: inc j (segment r i).
    apply /segmentP; apply /ordo_ltP => //.
    by apply: (ordinal_transitive oa ia).
  move : (proj1 (restriction1_fs ff sa1)) => fr.
  apply /(Vf_image_P1 fr).
  by rewrite sr1;exists j => //; rewrite (restriction1_V ff sa1 ji1).
case: (p_or_not_p (inc w (target f))) => wt; last first.
  have bf: (bijection f).
    split; last by exact.
    split; first by fct_tac.
    move => x y xsf ysf => sv.
    case: (equal_or_not (Vf f x) w) => le1.
       case: wt; rewrite -le1; Wtac.
    rewrite sf in xsf ysf.
    have ox: ordinalp x by ord_tac0.
    have oy: ordinalp y by ord_tac0.
    case: (ord_le_to_ell ox oy) => //.
       move /(ord_ltP oy) => lt2.
       by rewrite sv in le1; move: (fi _ ysf le1 _ lt2); rewrite sv.
    move /(ord_ltP ox) => lt2.
    by move: (fi _ xsf le1 _ lt2).
  have st: sub (target f) d.
    move=> t td; move: (stf _ td); case/setU1_P => // tw; case: wt;ue.
   move: (sub_smaller st).
  have <-: (cardinal (source f) = cardinal (target f))
       by apply /card_eqP; exists f;split => //.
  rewrite sf (card_card ca) => le2; co_tac.
pose pri i := (inc i (source f) /\ Vf f i = w).
have [i0 oi0 iv0]: exists2 i, ordinalp i & pri i.
  rewrite /pri;move: ((proj2 sjf) _ wt) => [i iv1 iv2]; exists i => //.
  move: iv1. rewrite sf => ok ; ord_tac0.
move: (least_ordinal4 oi0 iv0).
set qi :=least_ordinal _ _;move=> [oq [qsf qv] ql].
rewrite sf in qsf;move: qv; rewrite (fv _ qsf) /lef /lew.
set c := complement _ _ => qv.
  case: (p_or_not_p (nonempty c)) =>h.
  move: (lewe _ h) => [] /setC_P [wd _] _; case: wp.
  by move: wd;rewrite /lew -/c qv.
set e := image_of_fun (restriction_to_segment r qi f).
have sr1 : (source (restriction_to_segment r qi f)) = qi.
    rewrite /restriction_to_segment /restriction1; aw.
    rewrite /r ordinal_segment //.
have sa1: sub (segment r qi) (source f) by rewrite sf - sr ;apply: sub_segment.
move : (proj1 (restriction1_fs ff sa1)) => fr.
have pa1: forall i, inc i qi ->(inc (Vf f i) d /\ Vf f i <> w).
  move => t tq.
  move: (ordinal_transitive oa qsf tq); rewrite - sf => tf.
  have tw:inc (Vf f t) (target f) by apply: Vf_target.
  move: (stf _ tw) => /setU1_P.
  case: (equal_or_not (Vf f t) w) => ww; last by case.
  have prt : (pri t) by split.
  move: (ql _ (ordinal_hi oq tq) prt) => h1.
  have oqi: ordinalp qi by ord_tac.
  move: tq => /(ord_ltP oqi) => ok; ord_tac.
have fv1: forall u, inc u qi -> (Vf (restriction_to_segment r qi f)u) = Vf f u.
  move => i iq.
  have ji1: inc i (segment r qi).
    apply /segmentP; apply /ordo_ltP => //.
    by apply: (ordinal_transitive oa qsf).
 by rewrite (restriction1_V ff sa1 ji1).
have de: d = e.
  set_extens t.
    move: h; rewrite /c -/e => qa qb; ex_middle tne; case: qa.
    exists t; apply /setC_P;split => //.
  move /(Vf_image_P1 fr); rewrite sr1; move => [u uq ->].
  by rewrite (fv1 _ uq); move: (pa1 _ uq) => [].
have ij1: forall i j, inc i qi -> inc j qi -> Vf f i = Vf f j -> i = j.
  move => i j iq jq sv.
  move: (pa1 _ iq) (pa1 _ jq)=> [_ xa1] [_ ya1].
  have ia: inc i a by ord_tac0.
  have ja: inc j a by ord_tac0.
  have oi: ordinalp i by ord_tac0.
  have oj: ordinalp j by ord_tac0.
  case: (ord_le_to_ell oi oj) => //.
   by move /(ord_ltP oj) => lt2; move: (fi _ ja ya1 _ lt2); rewrite sv.
  by move /(ord_ltP oi) => lt2; move: (fi _ ia xa1 _ lt2).
have ij2: injection (restriction_to_segment r qi f).
    split; first by exact.
    rewrite sr1; move => x y xsf ysf /=.
    by rewrite (fv1 _ xsf) (fv1 _ ysf); apply: ij1.
move: (restriction_to_image_fb ij2).
set g := restriction_to_image (restriction_to_segment r qi f).
have tg: target g = d.
  by rewrite /g de /restriction_to_image/ restriction2; aw.
have osd: ordinalp (source g).
   rewrite /g /restriction_to_image/ restriction2 sr1; aw.
move: (restriction_to_image_fb ij2) => bg.
have fg: function g by fct_tac.
have r2a: restriction2_axioms (restriction_to_segment r qi f)
   (source (restriction_to_segment r qi f))
   (image_of_fun (restriction_to_segment r qi f)).
  by split => //; apply: fun_image_Starget.
have gV : forall i, inc i qi -> Vf g i = Vf f i.
  move => i iq; rewrite/g /restriction_to_image restriction2_V // ? fv1 ? sr1//.
exists g; split => // u v.
rewrite composef_domain => us vs uv; bw; rewrite -/(Vf g u) -/ (Vf g v).
have aux: domain (graph g) = qi.
  rewrite (f_domain_graph fg) /g /restriction_to_image /restriction2 corresp_s.
  aw; rewrite sr1.
rewrite aux in us vs; rewrite (gV _ us) (gV _ vs).
move: (pa1 _ us) => [wfu wfuw].
case: (equal_or_not u v) => euv.
   by rewrite - euv; apply: card_leR; apply: pb.
move: (ordinal_transitive oa qsf us) => ua.
rewrite (fv _ ua) /lef /lew; set c1:= nonempty _.
case: (p_or_not_p c1) => c1e; last first.
  by case: wfuw; rewrite (fv _ ua) /lef /lew; Ytac0.
move: (lewe _ c1e); rewrite /lew.
set f0:= (restriction_to_segment r u f); set x := Yo _ _ _; move=> [qa qb].
suff: inc (Vf f v)(d -s (image_of_fun f0)).
  move => qc; apply: (qb _ qc).
have sa2: sub (segment r u) (source f) by rewrite sf - sr ;apply: sub_segment.
have sr2 : (source (restriction_to_segment r u f)) = u.
    rewrite /restriction_to_segment /restriction1; aw.
    rewrite /r ordinal_segment //.
move : (proj1 (restriction1_fs ff sa2)) => fr2.
move: (pa1 _ vs) => [wfv _]; apply /setC_P;split => //.
move /(Vf_image_P1 fr2); rewrite sr2; move => [t tu].
have tu1: inc t (segment r u) by apply/segmentP; apply/ordo_ltP => //; ord_tac0.
rewrite (restriction1_V ff sa2 tu1) => sv1; symmetry in sv1.
have tqi: inc t qi by ord_tac0.
move: tu; rewrite (ij1 _ _ tqi vs sv1).
have ou: ordinalp u by ord_tac.
move /(ord_ltP ou)=> lt2; ord_tac.
Qed.

Definition cardinal_pos_fam g := (allf g (fun z => \0c <c z)).

Lemma compare_sum_prod5 x :
  fgraph x -> cardinal_pos_fam x ->
  (\csup (range x)) <=c (card_prod x).
Proof.
move => fx xi.
set A := Zo (domain x) (fun a => \2c <=c (Vg x a)).
have pa: (forall i, inc i ((domain x) -s A) -> (Vg x i) = \1c).
  move=> i /setC_P [idx ] /Zo_P h.
  move: (xi _ idx) => [xx yy]; ex_middle x1; case: h; split => //.
  by apply: card_ge2; [co_tac | apply:nesym |].
have Ax: sub A (domain x) by apply: Zo_S.
set g := (Lg A (Vg x)).
have fgg: fgraph g by rewrite /g ; fprops.
have dg: domain g = A by rewrite /g; bw.
have gs: (forall i : Set, inc i (domain g) -> \2c <=c Vg g i).
  by rewrite /g dg => i iA; bw; move: iA => /Zo_P [_].
move: (compare_sum_prod1 gs); rewrite (cprod_one_unit Ax pa) - /g.
have cs: cardinal_set (range x).
  move => t /(range_gP fx) [z zy ->]; move: (xi _ zy) => aux; co_tac.
case: (emptyset_dichot A) => Ae.
   move => _.
   have pb: union (range x) <=c \1c.
     apply: card_ub_sup => //; fprops.
     move => i /(range_gP fx) [j jy ->].
     have ja: inc j ((domain x) -s A)
        by apply /setC_P;split => //;rewrite Ae;case; case.
   rewrite (pa _ ja); fprops.
   rewrite /card_prodb cprod_trivial //; bw.
apply: card_leT.
have pb: (forall a, inc a (domain g) -> cardinalp (Vg g a)).
  move => a /gs => h; co_tac.
move: Ae => [a Aa]; move: (Aa) => /Zo_P [ay].
have ->: Vg x a = Vg g a by rewrite /g;bw.
rewrite -dg in Aa; move: (csum_increasing6 pb Aa).
move => le1 le2; move: (card_leT le2 le1) => le3.
apply: card_ub_sup => //; first by rewrite /card_sum; fprops.
move=> i /(range_gP fx) [j jdx ->].
have s1: \1c <=c card_sum g.
  move: (card_le_succ0 CS1); rewrite succ_one => h; co_tac.
case: (inc_or_not j A) => jA.
   rewrite -dg in jA; move: (csum_increasing6 pb jA).
   rewrite {1}/g; bw; ue.
have jc: inc j ((domain x) -s A) by apply /setC_P;split => //.
by rewrite (pa _ jc).
Qed.

Lemma infinite_increasing_power_bound1 X:
  fgraph X -> ordinal_fam X ->
  limit_ordinal (\osup (range X)) ->
  card_prod (Lg (domain X) (fun z => \aleph (Vg X z))) <=c
  \aleph (\osup (range X)) ^c (cardinal (domain X)).
Proof.
move => fX ogx ob.
have ->: omega_fct (union (range X)) ^c cardinal (domain X) =
   omega_fct (union (range X)) ^c (domain X).
  apply cpow_pr; fprops.
rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing; bw; fprops.
move => i idx; bw; apply: aleph_le_lec.
apply: ord_sup_ub.
  move => t tx; move: tx => /(range_gP fX) [z zi ->]; apply: (ogx _ zi).
apply /(range_gP fX); exists i => //;ue.
Qed.

Lemma infinite_increasing_power4 X (Y:= Lg (domain X)(fun z => \aleph (Vg X z)))
  (a := \osup (range X)):
  ofg_Mlt_lto X -> limit_ordinal (domain X) ->
  (cardinal (domain X) <=c \aleph a /\ \aleph a <c (card_prod Y)).
Proof.
move => pa pb.
move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe].
move: pa => [fgx xo xi].
move: (pc)(pb) => [oa _ _] [odx _ ldx].
have pa: cardinal (domain X) <=c (cardinal a).
  set f := Lf (Vg X) (domain X) (range X).
  have bf:bijection f.
    apply: lf_bijective.
        move => t td; apply /(range_gP fgx); ex_tac.
      move => u v ud vd sv.
      case: (ord_le_to_ell (ordinal_hi odx ud)(ordinal_hi odx vd)) => // cuv.
        by move: (xi _ _ ud vd cuv); rewrite sv;move => [_].
      by move: (xi _ _ vd ud cuv); rewrite sv;move => [_].
    move => y /(range_gP fgx) [x xd ->]; ex_tac.
  have ->: (cardinal (domain X)) = (cardinal (range X)).
   apply /card_eqP; exists f;split => //; rewrite /f; aw.
  apply: (sub_smaller pd).
move: (ordinal_cardinal_le1 (aleph_pr6 oa)).
rewrite (card_card (CS_aleph oa)) => lt1.
move: (card_leT pa lt1) => le1 {pa lt1}.
split; first by exact.
have ia: infinite_c (omega_fct a) by apply: (aleph_pr5c (proj31 pc)).
have cfy: cardinal_fam Y.
  rewrite /Y;hnf;bw; move => i idx; bw; apply: CS_aleph;fprops.
have fgY: fgraph Y by rewrite /Y; fprops.
have cd1: cardinal (domain Y) <=c omega_fct a by rewrite /Y; bw.
have <-: card_sum Y = \aleph a.
  by rewrite /Y - pe; apply: csum_of_small_b4 => //; rewrite pe.
set Z := Lg (domain X) (fun z => (omega_fct (Vg X (succ_o z)))).
have fgZ: fgraph Z by rewrite /Z; fprops.
have sd: domain Y = domain Z by rewrite /Y /Z; bw.
have inc1: (forall i, inc i (domain Y) -> Vg Y i <c Vg Z i).
  rewrite /Y/Z; bw; move => i idx; bw; apply: aleph_lt_ltc.
  apply: xi => //; [ by apply: ldx | apply: ord_succ_lt; ord_tac0].
apply: (card_lt_leT (compare_sum_prod fgY fgZ sd inc1)).
set X1 := fun_image (domain X) succ_o.
set f := Lf succ_o (domain X) X1.
have ta: lf_axiom succ_o (domain X) X1 by move => t td; apply /funI_P; ex_tac.
have bf: bijection f.
  rewrite /f/X1;apply: lf_bijective => //.
     move => u v ud vd; apply: ord_succ_inj; ord_tac0.
  by move => y /funI_P.
set Yr:= restr Y X1.
have scx1: sub X1 (domain X) by move =>t /funI_P [z zd ->]; apply: ldx.
have fgYr: fgraph Yr by rewrite /Yr;fprops.
have tf: target f = domain Yr by rewrite /f /Yr; aw; bw; rewrite /Y; bw.
move: (cprod_Cn tf bf).
have ff: function f by fct_tac.
have <-: Z = (Yr \cf (graph f)).
  rewrite /composef /Z (f_domain_graph ff) /f; aw.
  apply: Lg_exten => x xd.
  have qa: inc (succ_o x) X1 by apply: ta.
  have qb: inc (succ_o x) (domain Y) by rewrite /Y; bw; apply: ldx.
  rewrite -/ (Vf f x) (lf_V ta xd) /Yr /Y; bw.
  by apply: scx1.
move => <-.
apply: cprod_increasing1 => //.
  by red;rewrite /Y; bw;move => x xd; bw; apply: aleph_nz; apply: xo.
rewrite /Y; bw.
Qed.

Lemma infinite_increasing_power5 X (Y:= Lg (domain X)(fun z => \aleph (Vg X z)))
  (a := \osup (range X)):
  ofg_Mlt_lto X -> limit_ordinal (domain X) ->
  [/\ omega_fct a <c card_prod Y,
     card_prod Y <=c \aleph a ^c cardinal (domain X) &
     \aleph a ^c cardinal (domain X) <=c \2c ^c \aleph a].
Proof.
move => pa pb.
move: (infinite_increasing_power4 pa pb) => [qa qb].
move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe].
move: pa => [fgx xo xi].
move: (infinite_increasing_power_bound1 fgx xo pc); rewrite -/Y -/a => le1.
split; [exact | exact |].
move: (cpow_Meqle (aleph_nz (proj31 pc)) qa).
rewrite -/a infinite_power1_b //; apply: (aleph_pr5c (proj31 pc)).
Qed.

Lemma infinite_increasing_power x (y := domain x):
   fgraph x -> infinite_c y -> cardinal_pos_fam x ->
   fg_Mle_lec x ->
   card_prod x = (\csup (range x)) ^c y.
Proof.
move => fx cy alz xi.
have osr: cardinal_set (range x).
  move => t /(range_gP fx) [z zy ->]; move: (alz _ zy) => aux; co_tac.
apply: card_leA.
   rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing => //; fprops; bw.
   move=>t td; bw; apply: card_sup_ub => //; apply /(range_gP fx); ex_tac.
move: (infinite_product_prop2 cy) => [f [bf sf tf] fp].
set g:= Lg y (fun z=> fun_image y (fun t => (Vf f (J t z)))).
have ff: function f by fct_tac.
have pa: partition_w_fam g (domain x).
  rewrite /g; split;fprops.
     apply: mutually_disjoint_prop; bw.
     move=> i j z iy jy; bw.
     move=> /funI_P [a ay av] /funI_P [b iby bv].
     rewrite av in bv.
     have asf: inc (J a i) (source f) by rewrite sf; fprops.
     have bsf: inc (J b j) (source f) by rewrite sf; fprops.
     exact (pr2_def (bij_inj bf asf bsf bv)).
   set_extens t.
     move /setUb_P; bw; move => [a ay];bw; move /funI_P => [b ny ->].
     rewrite -/y -tf; Wtac; rewrite sf; fprops.
   rewrite -/y -tf => ytf; move: (bij_surj bf ytf) => [z zs zv].
   move: zs; rewrite sf => /setX_P; rewrite -tf; move => [pz za zb].
   apply /setUb_P; exists (Q z) => //;bw; apply /funI_P.
   by exists (P z) => //; rewrite pz.
rewrite (cprod_An pa).
rewrite {1} /g; bw.
rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing => //; fprops; bw.
move=> a ay; bw.
set h := (restr x (Vg g a)).
have fgr: fgraph (restr x (Vg g a)) by rewrite /h;fprops.
have s1: sub (Vg g a) (domain x).
    rewrite /g => t; bw; move /funI_P => [z zy ->]; rewrite -/y - tf.
    Wtac; rewrite sf; fprops.
have pb: (forall b, inc b (domain h) -> \0c <c Vg h b).
   rewrite /h restr_d // => b bv.
   rewrite restr_ev //; exact: (alz _ (s1 _ bv)).
move: (compare_sum_prod5 fgr pb); rewrite -/h => le1.
have csh: cardinal_set (range h).
  move => t /(range_gP fgr) [u ud ->]; move: (pb _ ud) => aux; co_tac.
apply: (card_leT _ le1).
apply card_ub_sup => //; first by apply: CS_sup.
move => i /(range_gP fx) [j jdx ->].
rewrite -/y -tf in jdx; move:(bij_surj bf jdx) => [z zf <-].
move: (zf); rewrite sf => /setX_P [pz py qy].
move: (infinite_card_limit2 cy) => [oy _ yp].
have op: ordinal_pair z by split => //; apply: (ordinal_hi (proj1 (proj1 cy))).
set b0 := ((P z) \cup (Q z)); set b := succ_o b0.
have ib0y: inc b0 y by rewrite /b0;case: (ordering_pair1 op); move=> [_ -> ].
have iby: inc b y by apply yp.
move: (ordinal_hi oy iby) (ordinal_hi oy ay) => ob oa.
have opab: ordinal_pair (J b a) by split => //; aw; fprops.
have bsba: b <=o (b \cup a).
  by case: (ordering_pair1 opab); aw; move => [le ->] //; apply ord_leR.
have ult: (P z) \cup (Q z) <o (b \cup a).
  apply: (ord_lt_leT _ bsba); exact (ord_succ_lt (ordinal_hi oy ib0y)).
have nzj: z <> J b a by move => zj; case: (proj2 ult); rewrite zj; aw.
have sa: inc (Vf f (J b a)) (Vg g a)
   by rewrite /g; bw; apply /funI_P; ex_tac.
have wy: inc (Vf f z) y by rewrite - tf; Wtac.
have wy': inc (Vf f (J b a)) y by rewrite - tf; Wtac; rewrite sf; fprops.
have jsf: inc (J b a) (source f) by rewrite sf; fprops.
have sb: Vf f z <o Vf f (J b a).
  rewrite -(fp _ _ zf jsf); split => //.
  apply /graph_on_P1; split => //;
   [ apply /setX_P;split => // | fprops | by split => //; aw; left].
apply: (card_leT (xi _ _ wy wy' (proj1 sb))).
apply: card_sup_ub => //; apply /(range_gP fgr).
exists (Vf f (J b a)); rewrite /h => //; bw.
Qed.

Lemma power_cofinality x: \2c <=c x -> x <c x ^c (cofinality_c x).
Proof.
move=> x1; move: (cofinality_c_rw x1) => [pb pc _].
move: pc => [f [[pc pd] pe pf]].
set g := cst_graph (domain f) x.
have pg: fgraph g by rewrite /g/cst_graph; fprops.
have ph: domain f = domain g by rewrite /g/cst_graph; bw.
have pi: (forall i, inc i (domain f) -> (Vg f i) <c (Vg g i)).
 by move=> i idf; rewrite /g/cst_graph; bw;apply:pd.
by move: (compare_sum_prod pc pg ph pi); rewrite /g cpow_pr2 pe pf.
Qed.

Lemma power_cofinality1 x: infinite_c x -> x <c x ^c (\cf x).
Proof.
move => icx; rewrite -(cofinality_card icx); apply: power_cofinality.
by apply: infinite_ge_two.
Qed.

Lemma power_cofinality2 x: infinite_c x -> x <c \cf (\2c ^c x).
Proof.
move=> xi;move: (infinite_powerset xi).
set y:= (\2c ^c x); move => iy.
have cx: cardinalp x by move: xi => [].
move:(cofinality_infinite_cardinal iy) => ia.
case: (card_le_to_el (proj1 ia) cx) => le2 //.
have ynz: y <> \0c by apply: infinite_nz.
move: (cpow_Meqle ynz le2).
rewrite {3} /y - cpow_pow (square_of_infinite xi) -/y => le3.
move: (power_cofinality1 iy) => le4;co_tac.
Qed.

Lemma power_cofinality3: omega0 <c \cf (\2c ^c omega0).
Proof.
apply: power_cofinality2; split;by [apply: CS_omega | apply: omega_infinite].
Qed.

Lemma power_cofinality4 a b: infinite_c a -> infinite_c b ->
   b <c \cf (a ^c b).
Proof.
move=> ia ib.
have pi: infinite_c (a ^c b) by apply: infinite_pow2.
rewrite -(cofinality_card pi).
have p1: \2c <=c (a ^c b) by apply: infinite_ge_two.
move: (cofinality_c_rw p1); set c:= cofinality_c (a ^c b).
move=> [le1 pa pb].
move: pa => [f [[qa qb qc] qd]].
set g := cst_graph (domain f) (a ^c b).
have fgf: fgraph f by move: qa => [].
have fgg: fgraph g by rewrite /g /cst_graph; fprops.
have sd: domain f = domain g by rewrite /g/cst_graph; bw.
have ltv: (forall i, inc i (domain f) -> (Vg f i) <c (Vg g i)).
  by move=> i idf; rewrite /g/cst_graph; bw; apply: qb.
move: (compare_sum_prod fgf fgg sd ltv).
rewrite /g cpow_pr2 qd qc - cpow_pow => lt1.
case: (card_le_to_el (proj31 le1) (proj1 ib)) => // cb.
move: (product2_infinite1 cb ib) => pa.
have pc: a ^c (b *c c) <=c a ^c b.
  apply: cpow_Mlele => //; first by apply: infinite_nz.
  move: ia => [ca _]; fprops.
co_tac.
Qed.

Lemma power_cofinality5 x y: \2c <=c x -> infinite_c y ->
  y <c \cf (x ^c y).
Proof.
move => x2 icy.
have cx: cardinalp x by co_tac.
case: (card_le_to_ee cx (proj1 icy)) => aux.
  by rewrite (infinite_power1_a x2 aux icy); apply: power_cofinality2.
move: (ge_infinite_infinite icy aux) => icx.
exact: (power_cofinality4 icx icy).
Qed.

Lemma infinite_power7b x y:
  infinite_c x -> y <c \cf x ->
  x ^c y <=c cardinal (unionb (Lg x (functions y))).
Proof.
move=> icx yc.
have cx: cardinalp x by move: icx => [cx _].
have ox: ordinalp x by apply: OS_cardinal.
have ha:(forall f, function_prop f y x -> inc (\osup (image_of_fun f)) x).
  move => f fp; move: (fp) => [ff sf tf].
  set T := (image_of_fun f).
  have osT: ordinal_set T.
    move=> t /(Vf_image_P1 ff) [u usf ->].
    by apply: (ordinal_hi ox); rewrite - tf;Wtac.
  have ou: ordinalp (union T) by apply: OS_sup.
  apply /(ord_ltP ox);case: (ord_le_to_el ox ou) => // le1.
  have eq1: union T = x.
    apply: ord_leA => //; apply: ord_ub_sup => //.
    move=> i => /(Vf_image_P1 ff) [u usf ->].
    move: (Vf_target ff usf); rewrite tf => /(ord_ltP ox).
    by move => [].
  have cox: cofinal_function_ex x y.
    exists f; split => // => t tx.
    have ls: t <o \osup T by apply /(ord_ltP ou); ue.
    move: (ord_lt_sup osT ls) => [z].
    move /(Vf_image_P1 ff) => [u usf ->] [tw _].
    rewrite - sf; ex_tac.
  move: (cofinality_rw ox) => [_ _ h].
  have oy: ordinalp y by move: yc => [[[oy _] _] _].
  move: (h _ oy cox) => le.
  move: (ordinal_cardinal_lt yc) => yc1; ord_tac.
pose sf f := \osup (image_of_fun f).
pose sf1 f := succ_o (sf f).
have pa: forall f, inc f (functions y x) -> (sf1 f) <o x.
  move: (infinite_card_limit2 icx) => [qa qb qc].
  move => f /fun_set_P fp; apply /(ord_ltP ox); apply: qc; exact: (ha _ fp).
have pb:forall f, inc f (functions y x) ->
  (forall t, inc t (source f) -> inc (Vf f t) (sf1 f)).
  move => f /fun_set_P [ff srf tf] t tsf.
  have osT: ordinal_set (image_of_fun f).
      move=> z /(Vf_image_P1 ff) [u usf ->].
      by apply: (ordinal_hi ox); rewrite - tf;Wtac.
   apply /ord_leP; first by apply: OS_sup.
   apply: ord_sup_ub => //; apply /(Vf_image_P1 ff); ex_tac.
pose R f := restriction2 f (source f) (sf1 f).
have pc: forall f, inc f (functions y x) ->
  restriction2_axioms f (source f) (sf1 f).
  move=> f fp; move: (fp) => /fun_set_P [qc qd qe].
  split => //.
    by rewrite qe; move: (pa _ fp) => [[_ _ ok] _].
  by move=>t /(Vf_image_P1 qc) [u usf ->]; apply: (pb _ fp).
have pd: forall f, inc f (functions y x) ->
    inc (R f) (functions y (sf1 f)).
  move=> f fh; move: (restriction2_prop (pc _ fh)) => [p1 p2 p3].
  apply /fun_set_P;split => //; rewrite /R p2.
  by move: fh => /fun_set_P [q1 q2 q3].
set t1:= unionb _.
have pe: forall f, inc f (functions y x) -> inc (R f) t1.
  move=> f fi; move: (pd _ fi) => sa.
  have sb:inc (sf1 f) x by apply /(ord_ltP ox); exact: (pa _ fi).
  apply /setUb_P; bw; exists (sf1 f) => //; bw.
set g := Lf R (functions y x) t1.
suff ig: injection g by move: (incr_fun_morph ig); rewrite /g; aw.
apply: lf_injective => // u v us vs eq.
move: (pc _ us) (pc _ vs) => axf axg.
move: us vs => /fun_set_P [fu su tu] /fun_set_P [fv sv tv].
apply: function_exten => //; try ue.
move => t tsu; move: (f_equal (Vf ^~ t) eq);rewrite /R restriction2_V //.
by rewrite restriction2_V // sv - su.
Qed.

Lemma infinite_power2 n m (x:=\aleph n) (y:= \aleph (succ_o n)):
   ordinalp n -> m <> \0c ->
   y ^c m = (x ^c m) *c y.
Proof.
move => on mnz.
rewrite -(cpow_prb) -(cpow_prb x);set m':= cardinal m.
have cm': cardinalp m' by rewrite /m'; fprops.
have m'nz: m' <> \0c by dneg cmz; move: (cardinal_nonemptyset cmz).
have osn:= (OS_succ on).
move: (aleph_pr5c on) (aleph_pr5c osn) (aleph_pr10c on).
rewrite -/x -/y => icx icy ap.
have m1: \1c <=c m' by apply: card_ge1; fprops.
have p1: forall z, ordinalp z -> (\aleph z) <=c ((\aleph z) ^c m').
  move=> z oz; move: (aleph_pr5c oz) => iz; move: (iz) => [cz _].
  apply: cpow_Mle1 => // coz.
have ipx: infinite_c (x^c m') by apply: (infinite_pow).
move: (ap) => [lexy _].
have cxy := (cpow_Mleeq m' (proj1 ap) (aleph_nz on)).
move: (icy) => [cy _]; move:(cy) => [oy _].
apply: card_leA; last first.
  by apply: product2_infinite4 => //; [apply: p1 | apply:infinite_pow].
case: (card_le_to_el cy cm') => cmx.
  move: (ge_infinite_infinite icy cmx) => im.
  move: (infinite_ge_two icx) => lex2.
  rewrite (infinite_power1_a lex2 (card_leT lexy cmx) im).
  rewrite (infinite_power1_a (card_leT lex2 lexy) cmx im).
  apply: cprod_M1le => //.
     rewrite /card_pow; fprops.
  apply: (aleph_nz (OS_succ on)).
have ha: m' <c \cf y.
  by move: (regular_initial_successor on) => /regular_cardinalP [_ ->].
move: (infinite_power7b icy ha) => hb.
set t1 := (unionb (Lg y (functions m'))).
suff pb: cardinal t1 <=c (x ^c m') *c y by co_tac.
apply: (card_leT (csum_pr1 (Lg y (functions m')))).
rewrite /card_sumb; bw; set f := Lg _ _.
have df: domain f = y by rewrite /f; bw.
rewrite - df /f; apply:csum_of_small_b1.
split; [ fprops | hnf; bw; move =>i ix; bw].
rewrite -/(card_pow i m') - cpow_pra.
case: (equal_or_not (cardinal i) \0c) => iz.
  rewrite iz (cpow0x m'nz);apply: czero_least; rewrite /card_pow; fprops.
by apply: (cpow_Mleeq _ _ iz); apply: (aleph_pr12d on); apply /(ord_ltP oy).
Qed.

Lemma infinite_power2_bis x (y:= succ_c x) m:
  infinite_c x -> m <> \0c ->
   y ^c m = (x ^c m) *c y.
Proof.
move=> ix mnz; rewrite /y;move: (ord_index_pr1 ix)=> [on <-].
rewrite (succ_c_pr on); apply: (infinite_power2 on mnz).
Qed.

Lemma infinite_power3 n m (x:=\aleph n):
   inc n Bnat -> m <> \0c ->
   x ^c m = (\2c ^c m) *c x.
Proof.
move=> nB mz.
set m':= cardinal m.
have cm': cardinalp m' by rewrite /m'; fprops.
have m'nz: m' <> \0c by dneg cmz; move: (cardinal_nonemptyset cmz).
have ->: \2c ^c m = \2c ^c m' by rewrite /m';apply: cpow_pr; fprops.
have ->: x ^c m = x ^c m' by rewrite /m';apply: cpow_pr; fprops.
rewrite /x; clear x.
case: (finite_dichot cm') => fm.
  have mB: inc m' Bnat by apply /BnatP.
  have on: ordinalp n by apply: (ordinal_hi OS_omega nB).
  move: (aleph_pr5c on) => io.
  rewrite (power_of_infinite io mB m'nz) cprodC.
  symmetry; apply: product2_infinite => //; last by apply: cpow2_nz.
  apply: finite_le_infinite => //; bw.
  apply /BnatP; apply: BS_pow; fprops.
have io: infinite_c omega0 by rewrite - aleph_pr1; apply: aleph_pr5c; fprops.
have pa: \2c <=c omega0 by apply: infinite_ge_two.
have onz: omega0 <> \0c by apply: omega_nz.
move: n nB; apply: cardinal_c_induction.
  rewrite aleph_pr1.
  have le1: omega0 <=c m'.
   by split => //;[ apply: CS_omega|apply: omega_limit3].
  move: (card_leT le1 (proj1 (cantor cm'))) => le2.
  rewrite infinite_power1_a // product2_infinite //.
  apply: (ge_infinite_infinite io le2).
move=> n nB hrec.
rewrite succ_of_finite; last by apply /BnatP.
have on: ordinalp n by apply: (ordinal_hi OS_omega nB).
rewrite (infinite_power2 on m'nz) hrec - cprodA.
move: (aleph_pr10c on) => [pc _].
move: (product2_infinite pc (aleph_pr5c (OS_succ on)) (aleph_nz on)).
by rewrite cprodC; move => ->.
Qed.

Lemma infinite_power4 a (b:= \2c ^c a): infinite_c a ->
  [/\ b ^c a = b, b ^c a <c (succ_c b) ^c a,
    (forall c, \2c <=c c -> c ^c a = c -> b <=c c) &
     (forall c, infinite_c c -> c ^c a <c (succ_c c) ^c a -> b <=c c)].
Proof.
move=> ica.
have anz: a <> \0c by apply: infinite_nz.
have ib: infinite_c b by apply: infinite_powerset.
have p1: b ^c a = b by rewrite/b - cpow_pow square_of_infinite.
have p3: (forall c, \2c <=c c -> c ^c a = c -> b <=c c).
   move =>c c2 cp.
   have cc: cardinalp c by co_tac.
   case: (card_le_to_el (proj1 ib) cc) => //; move=> [le1 ne1].
   move: (infinite_power1 c2 le1 ica); rewrite cp -/b //.
have p2: b ^c a <c succ_c b ^c a.
  move: (proj32 (succ_c_pr1 (proj1 ib))).
  rewrite (infinite_power2_bis ib anz) p1 => h; move: (proj1 h) => le1.
  move: (infinite_nz ib) => bnz.
  have isc: infinite_c (succ_c b) by apply: (ge_infinite_infinite ib le1).
  by rewrite cprodC (product2_infinite le1 isc bnz).
split => //.
move=> c ic; rewrite (infinite_power2_bis ic anz).
have c1: cardinalp (c ^c a) by fprops.
have c2 := (CS_succ_c (proj1 ic)).
case: (card_le_to_el c2 c1) => h.
  have ip: infinite_c (c ^c a) by apply: infinite_pow2.
  move: (product2_infinite1 h ip) => q1 q2; co_tac.
move: (succ_c_pr4 (proj1 ic) h) => h1 _.
apply: (p3 _ (infinite_ge_two ic)).
apply: card_leA => //; apply: cpow_Mle1; [by co_tac | done].
Qed.

Lemma infinite_power5 n p m (x:=\aleph n) (y:= \aleph (n +o p)):
   ordinalp n -> ordinalp p -> cardinalp m -> m <> \0o ->
   cardinal p <=c m ->
   y ^c m = (x ^c m) *c (y ^c (cardinal p)).
Proof.
move=> on op cm mnz cpm.
have ca: cardinalp (x ^c m) by rewrite /card_pow; fprops.
pose hyp p:= cardinal p <=c m ->
  \aleph (n +o p) ^c m = x ^c m *c \aleph (n +o p) ^c (cardinal p).
case:(least_ordinal6 hyp op); first by apply.
set q :=least_ordinal _ _; move=> [oq pb] [] => pa.
have xnz: x <> \0c by apply: aleph_nz.
move: (pa); rewrite - {1} (card_card cm) => pa'.
case: (limit_ordinal_pr2 oq) => h.
   rewrite h cardinal_set0 (osum0r on) cpowx0 cprod1r //.
  move:h=> [r or qv].
  rewrite qv - osum2_succ //.
  have rq1: inc r q by rewrite qv; fprops.
  have cq:= (card_leT (sub_smaller (ordinal_transitive oq rq1)) pa).
  move: (pb _ rq1 cq).
  set y1 := \aleph (n +o r); set y2 := \aleph (succ_o (n +o r)).
  have onr: ordinalp (n +o r) by fprops.
  move: (infinite_power2 onr mnz); rewrite -/y1 -/y2 => r1 r2.
  have osnr: ordinalp (succ_o (n +o r)) by fprops.
  have cy1m: cardinalp (y1 ^c m) by rewrite /card_pow; fprops.
  have icy2: infinite_c y2 by apply: aleph_pr5c.
  have icy1: infinite_c y1 by apply: aleph_pr5c.
  have icx: infinite_c x by apply: aleph_pr5c.
  have y1nz: y1 <> \0c by apply: aleph_nz.
  have y2nz: y2 <> \0c by apply: aleph_nz.
  move: (icy1) (icy2) (icx) => [cy1 _ ] [cy2 _] [cx _].
  have xx: x <=c x by fprops.
  have y1y1: y1 <=c y1 by fprops.
  have y2y2: y2 <=c y2 by fprops.
  have le1: x ^c m <=c y1 ^c m.
      have xy1: x <=c y1.
        by apply: aleph_le_lec; apply (osum_Mle0 on or).
      by apply: cpow_Mleeq.
  have le0: y1 <=c y2.
    by apply: aleph_le_lec; exact (proj1 (ord_succ_lt (OS_sum2 on or))).
  have le2: y1 ^c m <=c y2 ^c m by apply: cpow_Mleeq.
  have paa: x <=c x ^c m by apply: cpow_Mle1 => //.
  have lexx: y2 ^c (succ_o r) <=c y2 ^c m.
     by rewrite - qv; exact (cpow_Meqle0 y2nz pa').
  move: (ge_infinite_infinite icx paa) => icxm.
  move: (ge_infinite_infinite icxm le1) => icy1m.
  move: (ge_infinite_infinite icy1m le2) => icy2m.
  have y1mnz: y1 ^c m <> \0c by apply: (cpow_nz y1nz).
  have xmnz: x ^c m <> \0c by apply: (cpow_nz xnz).
  have saux2: y2 ^c cardinal (succ_o r) = y2 ^c (succ_o r)
   by apply: cpow_pr; fprops.
  case: (card_le_to_ee cy1m cy2) => r3.
    move: (product2_infinite r3 icy2 y1mnz).
    rewrite cprodC; move=> h; rewrite h in r1.
    rewrite r1; rewrite r1 in lexx.
    rewrite saux2 (card_leA lexx (cpow_Mle1 cy2 (@succo_nz r))).
    have r6: x ^c m <=c y2 by rewrite -r1; co_tac.
    by rewrite cprodC (product2_infinite r6 icy2 xmnz).
  move: (product2_infinite r3 icy1m y2nz) => r4.
  rewrite r4 in r1.
  have saux: y1 ^c cardinal r = y1 ^c r by apply: cpow_pr; fprops.
  have r6: y2 ^c (succ_o r) <> \0c by apply: (cpow_nz y2nz).
  case: (equal_or_not (x ^c m) (y1 ^c m)) => r7.
     rewrite r7 -r1.
     by rewrite saux2 (product2_infinite lexx icy2m r6).
  have r8: x ^c m <c y1 ^c m by split.
  have r9: y1 ^c m = y1 ^c r.
    have c1: cardinalp (x ^c m) by rewrite /card_pow; fprops.
    have c2: cardinalp (y1 ^c r) by rewrite /card_pow; fprops.
    case: (card_le_to_ee c1 c2) => h.
      have it: infinite_c (y1 ^c r)
        by apply: (ge_infinite_infinite icxm h).
      move: (product2_infinite h it xmnz); rewrite cprodC => xx1.
      by rewrite r2 - xx1 saux.
    have nzyr: y1 ^c r <> \0c by apply: (cpow_nz y1nz).
    by move:(product2_infinite h icxm nzyr) r2; rewrite saux => -> ww; case: r7.
  have crr1:cardinal r <=c cardinal (succ_o r).
      apply: sub_smaller; rewrite /succ_o; fprops.
   move: (cpow_Mlele y1nz le0 crr1); rewrite saux saux2.
   rewrite -r9 -r1 => le3; rewrite (card_leA lexx le3) cprodC.
   by rewrite (product2_infinite (card_leT le1 le2) icy2m xmnz).
have onq: ordinalp (n +o q) by apply: OS_sum2 => //; ord_tac0.
apply card_leA; last first.
   move: (infinite_pow (aleph_pr5c onq) mnz) => r1.
   have r0: x <=c \aleph (n +o q).
     by apply: aleph_le_lec; apply osum_Mle0.
   have r2: x ^c m <=c \aleph (n +o q) ^c m.
      apply: (cpow_Mleeq _ r0 (aleph_nz on)).
   apply: (product2_infinite4 r2 _ r1).
     apply: cpow_Meqle => //; apply: (aleph_nz onq).
set E := (fun_image q (fun z => \aleph (n +o z))).
set f := Lg q (fun z : Set => \aleph (n +o z)).
have r2: E = range f by rewrite Lg_range.
have r1 : \aleph (n +o q) = \osup E.
  move: (normal_ofs_compose aleph_pr11 (osum_normal on)) => [xa xb].
  move: (xb _ h) => /= ->; congr (union _); set_extens; aw.
have fgf: fgraph f by rewrite /f; fprops.
have r3: forall i, inc i (domain f) -> \2c <=c Vg f i.
   rewrite /f; bw; move=> i idf; bw; apply: infinite_ge_two.
   apply: aleph_pr5c; apply: OS_sum2 => //; ord_tac.
have r4: \aleph (n +o q) = card_sum f.
   rewrite r1 r2 - csum_of_small_b4 //.
     move=> a ad; move: (r3 _ ad)=> aux; co_tac.
   rewrite -r2 -r1; apply: aleph_pr5c => //.
   rewrite - r2 -r1 /f; bw.
   have r5: q <=o n +o q by apply: osum_M0le.
   apply:card_leT (aleph_le_lec r5).
   move: (ordinal_cardinal_le1 (aleph_pr6 oq)).
   rewrite (card_card (CS_aleph oq)) //.
have r5: \aleph (n +o q) <=c card_prod f.
   rewrite r4; apply: compare_sum_prod2 => //.
   move=> i idf; move: (r3 _ idf) => [_ c _]; fprops.
move: (cpow_Mleeq m r5 (aleph_nz onq)).
rewrite cpow_prod {1} /f; bw.
rewrite /card_prodb.
have ->: (Lg q (fun i : Set => Vg f i ^c m)) =
   Lg q (fun t => x ^c m *c \aleph (n +o t) ^c (cardinal t)).
  apply: Lg_exten; move=> t tq.
  have tq1: t <o q by apply /(ord_ltP oq).
  rewrite /f; bw; apply (pb _ tq); apply: (card_leT _ pa).
  apply:(ordinal_cardinal_le1 (proj1 tq1)).
rewrite -/(card_prodb q _).
rewrite -prod_of_prods /card_prodb cpow_pr2 - cpow_pow.
have icq: infinite_c (cardinal q).
rewrite /infinite_c.
  have aux: infinite_c (cardinal omega0).
    apply /infinite_setP; apply: infinite_Bnat.
  apply: ( ge_infinite_infinite aux).
  exact (sub_smaller (proj33 (omega_limit2 h))).
have ->: x ^c (m *c q) = x ^c m.
  move: (ge_infinite_infinite icq pa) => icm.
  move: (product2_infinite pa icm (infinite_nz icq)).
  by rewrite cprod2_pr2b => ->.
set f2:= \aleph (n +o q) ^c (cardinal q).
set ff:= (fun i : Set => \aleph (n +o i) ^c (cardinal i)).
move => r6.
have: card_prod (Lg q ff) <=c f2 ^c (cardinal q).
   rewrite cpow_prb - cpow_pr2/cst_graph.
   apply: cprod_increasing; bw.
   move=> t tq; rewrite {1} (LVg_E ff tq) {1} (LVg_E _ tq).
   have [tq1 _]: t <o q by apply /ord_ltP.
   have ntq: n +o t <=o n +o q by apply: osum_Meqle.
   apply: cpow_Mlele.
   - by apply: aleph_nz; ord_tac.
   - by apply: aleph_le_lec.
   - by apply ordinal_cardinal_le1.
have ->: f2 ^c (cardinal q) = f2.
   by rewrite /f2 - cpow_pow; congr card_pow; apply: square_of_infinite.
move=> r7; apply: (card_leT r6); apply: cprod_Mlele => //; fprops.
Qed.

Lemma infinite_power6 p m (y:= \aleph p):
  ordinalp p -> cardinalp m -> m <> \0o ->
   cardinal p <=c m ->
   (infinite_c m \/ p <> \0o) ->
   y ^c m = (\2c ^c m) *c (y ^c (cardinal p)).
Proof.
move=> op cm mz cpm dc.
move: (infinite_power5 OS0 op cm mz cpm).
rewrite (osum0l op) -/y aleph_pr1. move => ->.
move: omega_infinitec => pa.
move:(infinite_ge_two pa) => aux.
case: (finite_dichot cm) => fm; last first.
  congr card_prod2; apply infinite_power1_a => //.
  move:(sub_smaller (omega_limit3 fm));rewrite !card_card //; exact CS_omega.
case: dc => pz; first by case: (infinite_dichot1 fm pz).
have mb: inc m Bnat by apply /BnatP.
have mpb: inc (cardinal p) Bnat by apply (BS_le_int cpm mb).
rewrite (power_of_infinite pa mb mz).
have cpz: cardinal p <> \0o by move=> h; move: (cardinal_nonemptyset h).
move: (aleph_pr5c op)=> iy.
have le1: omega0 <=c \aleph p.
  by rewrite - aleph_pr1; apply: aleph_le_lec; by apply: ozero_least.
have le2: \2c ^c m <=c \aleph p.
  apply: card_leT le1.
  apply: finite_le_infinite => //;apply /BnatP; apply: BS_pow; fprops.
move: (power_of_infinite iy mpb cpz).
have -> : \aleph p ^c cardinal p = \aleph p ^c p by apply: cpow_pr; fprops.
move ->.
rewrite cprodC; rewrite (product2_infinite le1 iy omega_nz).
rewrite cprodC; rewrite (product2_infinite le2 iy) //.
apply: cpow2_nz.
Qed.

Lemma infinite_power6_0 p m (y:= \aleph p):
  ordinalp p -> infinite_c m -> cardinal p <=c m ->
   y ^c m = (\2c ^c m) *c (y ^c (cardinal p)).
Proof.
move=> op icm cp.
have aux: (infinite_c m \/ p <> \0o) by left.
by rewrite (infinite_power6 op (proj1 icm) (infinite_nz icm) cp aux).
Qed.

Lemma infinite_power6_1 a: a <o omega1 ->
  (\aleph a) ^c aleph1 =
  (\aleph a) ^c aleph0 *c \2c ^c aleph1.
Proof.
move => ao.
have oa: ordinalp a by ord_tac.
have coo: cardinalp (\aleph \1o) by apply: CS_aleph; fprops.
move: ao => /(ordinal_cardinal_le2P coo oa) ao.
rewrite /aleph0 - aleph_pr1.
move: (aleph_nz oa) => xnz.
apply: card_leA.
   rewrite (infinite_power6_0 oa (aleph_pr5c OS1) (proj1 ao)) cprodC.
   apply: cprod_Mlele; last by apply: card_leR; fprops.
   by apply: cpow_Meqle => //;apply: (aleph_pr10a OS0); rewrite succ_o_zero.
move: (aleph_pr5c oa) => ioa.
apply: product2_infinite4.
- apply: cpow_Meqle => //; apply: aleph_le_lec; apply: ozero_least; fprops.
- apply: cpow_Mleeq; [ apply: finite_le_infinite | ]; fprops.
- apply: infinite_pow => //; apply: aleph_nz; fprops.
Qed.

Lemma infinite_power6_2 a: a <o omega2 ->
  (\aleph a) ^c aleph2 =
  (\aleph a) ^c aleph1 *c \2c ^c aleph2.
Proof.
move => ao.
have oa: ordinalp a by ord_tac.
have coo: cardinalp aleph2 by apply: CS_aleph; fprops.
move: ao => /(ordinal_cardinal_le2P coo oa) => ao.
move: (aleph_nz oa) => xnz.
apply: card_leA.
   rewrite (infinite_power6_0 oa (aleph_pr5c OS2) (proj1 ao)) cprodC.
   apply: cprod_Mlele; last by apply: card_leR; fprops.
   by apply: cpow_Meqle => //;apply: (aleph_pr10a OS1); rewrite succ_o_one.
move: (aleph_pr5c oa) => ioa.
apply: product2_infinite4.
- apply: cpow_Meqle => //;apply: aleph_le_lec;apply: ord_ge1; fprops.
- apply: cpow_Mleeq; [ apply: finite_le_infinite |];fprops.
- apply: infinite_pow => //; apply: aleph_nz; fprops.
Qed.

Lemma infinite_power6_3:
  (\aleph omega0) ^c aleph1 =
  (\aleph omega0) ^c aleph0 *c \2c ^c aleph1.
Proof.
apply: infinite_power6_1.
rewrite - aleph_pr1; apply: aleph_lt_lto; apply: ord_lt_01.
Qed.

Lemma infinite_power6_4 a b:
  infinite_o a -> a <o omega1 -> ordinalp b ->
  (\aleph a) ^c (\aleph b) =
  (\aleph a) ^c aleph0 *c \2c ^c (\aleph b).
Proof.
move => ioa a1 ob.
have oa: ordinalp a by ord_tac.
move: (aleph_pr5c ob) => iob.
move: (a1) => /(ordinal_cardinal_le2P (CS_aleph OS1) oa).
rewrite - succ_o_zero => ca; move: (aleph_pr10a OS0 ca) => ca1.
have ca2: cardinal a <=c \aleph b.
  by apply: (card_leT ca1); apply aleph_le_lec; apply: ozero_least.
rewrite (infinite_power6_0 oa iob ca2) cprodC.
suff: cardinal a = aleph0 by move ->.
rewrite /aleph0 - aleph_pr1; apply: card_leA => //; rewrite aleph_pr1.
by move/(omega_P1 oa): ioa => /sub_smaller; rewrite (card_card CS_omega).
Qed.

Lemma infinite_power6_5 a b c :
  ordinalp a -> ordinalp b ->
  \aleph (\omega a) = c ^c (\aleph b) ->
  b <o a.
Proof.
move => oa ob.
move: (aleph_limit oa) => la.
have aux: infinite_c (\aleph (\aleph a)).
  by apply: aleph_pr5c; apply: OS_aleph.
have ->: c ^c \omega b =(cardinal c) ^c \omega b by apply:cpow_pr; fprops.
set C := cardinal c.
case: (equal_or_not C \1c) => eq1.
  rewrite eq1 cpow1x =>h; move: aux; rewrite h; move: finite_1.
  move => pa pb; case: (infinite_dichot1 pa pb).
case: (equal_or_not C \0c) => eq0.
  rewrite eq0 cpow0x =>h. move: aux; rewrite h; move: finite_0.
    move => pa pb; case: (infinite_dichot1 pa pb).
  by case: (aleph_nz ob).
move: (card_ge2 (CS_cardinal c) eq0 eq1) => c2 h.
move: (power_cofinality5 c2 (aleph_pr5c ob)).
rewrite - (f_equal cofinality h).
rewrite regular_initial_limit1 //.
move: (aleph_pr5c oa) => ia.
move: (cofinality_small ia) => l1 l2.
exact: (aleph_ltc_lt ob oa (card_lt_leT l2 l1)).
Qed.

Lemma infinite_power6_6 n : ordinalp n ->
 \2c ^c (\aleph omega0) = \aleph (\omega n) -> omega0 <o n.
Proof.
move => on h3; symmetry in h3.
exact (infinite_power6_5 on OS_omega h3).
Qed.

Lemma infinite_power6_5a a b : infinite_c b ->
 \aleph omega1 = a ^c b -> b = aleph0.
Proof.
move => /ord_index_pr1; set n := ord_index b;move => [on <-] eq.
by move:(infinite_power6_5 OS1 on eq) => /ord_lt1 ->; rewrite aleph_pr1.
Qed.

Definition gimel_fct x := x ^c (\cf x).

Lemma gimel_prop1 x: regular_cardinal x ->
  \2c ^c x = gimel_fct x.
Proof.
by move=> /regular_cardinalP[ic xc]; rewrite /gimel_fct xc infinite_power1_b.
Qed.

Lemma gimel_prop2 x: infinite_c x ->
  gimel_fct x <=c \2c ^c x.
Proof.
move=> ic; rewrite /gimel_fct - (infinite_power1_b ic).
move: (cofinality_small ic) => cg.
apply: cpow_Mlele => //; [ by apply: infinite_nz | apply: card_leR; co_tac].
Qed.

Lemma infinite_power6_7a: \2c ^c aleph1 = aleph2 ->
 \aleph omega0 ^c aleph1 = \aleph omega0 ^c aleph0.
Proof.
move => pa; move: infinite_power6_3; rewrite pa.
have pc: aleph2 <=c \aleph omega0 ^c aleph0.
  have l1: aleph2 <=c \aleph omega0.
    apply: aleph_le_lec; apply: ord_le_2omega.
    have co: cardinalp (\aleph omega0) by co_tac.
    apply: (card_leT l1); apply: cpow_Mle1 => //; last by apply: omega_nz.
move: (aleph_pr5c OS2) => i2.
move: (ge_infinite_infinite i2 pc) => i3.
by rewrite (product2_infinite pc i3 (infinite_nz i2)).
Qed.

Lemma infinite_power6_7b:
  \2c ^c aleph1 = aleph2 ->
  (\aleph omega0) ^c aleph0 <> \aleph omega1.
Proof.
move => pa pb.
move: (infinite_power6_7a pa); rewrite pb => aux; symmetry in aux.
rewrite - (aleph_pr1) in pb.
move: (infinite_power6_5 OS1 OS1 aux); by move => [].
Qed.

Lemma infinite_power6_7c:
  \2c ^c aleph1 = aleph2 ->
   \aleph omega1 <c (\aleph omega0) ^c aleph0 ->
  \aleph omega1 ^c aleph1 = (\aleph omega0) ^c aleph0.
Proof.
set x1 := \aleph omega1.
set x2 := \aleph omega0 ^c aleph0.
move => pa [pb _].
have pc: \aleph omega0 <> \0c by apply: (aleph_nz OS_omega).
have x1nz: x1 <> \0c by apply: aleph_nz ; apply: OS_aleph; fprops.
have pd: aleph0 <=c aleph1.
  rewrite /aleph0 - aleph_pr1;apply: aleph_le_lec; apply: (ozero_least OS1).
have pe: \aleph omega0 <=c x1.
  by apply: aleph_le_lec; apply: (ordinal_cardinal_le).
have pf: x2 <=c x1 ^c aleph0 by apply: cpow_Mleeq.
symmetry;apply: card_leA.
  apply: (card_leT pf); apply: cpow_Meqle => //; apply: aleph_nz.
have: x1 ^c \aleph \1o <=c x2 ^c \aleph \1o by apply: cpow_Mleeq.
move: (infinite_power6_7a pa); rewrite -/x2 ; move => <-.
rewrite - cpow_pow square_of_infinite //;apply: aleph_pr5c; fprops.
Qed.

Lemma infinite_power6_7d:
  \aleph omega0 <c \2c ^c omega0 ->
  (\aleph omega0) ^c omega0 = \2c ^c omega0.
Proof.
move=> [h _ ].
move: (aleph_pr5c OS_omega) => io.
apply: card_leA; last first.
  apply cpow_Mleeq;[ by apply: infinite_ge_two | fprops].
move: (cpow_Mleeq omega0 h (infinite_nz io)).
rewrite - cpow_pow square_of_infinite //; apply: omega_infinitec.
Qed.

Lemma infinite_power6_7e:
   \aleph omega1 <=c \2c ^c omega0 ->
   (gimel_fct (\aleph omega0) = \2c ^c aleph0
   /\ gimel_fct (\aleph omega1) = \2c ^c aleph1).
Proof.
set o1 := \aleph \1o.
move => h; rewrite /gimel_fct.
have h1: \aleph omega0 <=c \aleph o1.
   rewrite - aleph_pr1; apply: aleph_le_lec; apply: aleph_le_leo.
   apply: ozero_least; fprops.
move: (card_leT h1 h) => h2.
move: (regular_initial_limit1 (aleph_limit OS0)); rewrite aleph_pr1.
move: (regular_initial_limit1 (aleph_limit OS1)); rewrite -/o1.
move: (aleph_pr5c OS_omega) => pa.
move => -> ->.
move: regular_omega => [_ ->].
move: card2_nz => cn2.
split.
   apply: card_leA.
     move: (cpow_Mleeq omega0 h2 (infinite_nz pa)).
     rewrite - cpow_pow square_of_infinite //; apply: omega_infinitec.
   apply: cpow_Mleeq => //; apply: finite_le_infinite => //; fprops.
move: (regular_initial_successor OS0).
rewrite succ_o_zero ; move=> [pb].
rewrite (cofinality_card pb) -/o1; move => ->.
move: (aleph_pr5c (proj1 (proj1 pb))); rewrite -/o1 => io1.
have aux: (omega0 *c o1) = o1.
   rewrite cprodC; apply: product2_infinite => //.
   rewrite - aleph_pr1; apply: aleph_le_lec; apply: ozero_least; fprops.
   apply: omega_nz.
apply: card_leA.
     move: (cpow_Mleeq o1 h (infinite_nz io1)).
     by rewrite - cpow_pow aux.
apply: cpow_Mleeq => //; apply: finite_le_infinite => //; fprops.
Qed.

Lemma infinite_power6_7f:
  \aleph omega0 <c (\aleph omega0) ^c omega0 /\
  \aleph omega1 <c (\aleph omega1) ^c omega1.
Proof.
set x := \aleph omega0.
set y := \aleph omega1.
have icx: infinite_c x by apply: aleph_pr5c; apply: OS_omega.
have icy: infinite_c y by apply: aleph_pr5c; apply: OS_aleph; fprops.
have la: limit_ordinal omega1 by apply: aleph_limit; fprops.
split.
  move: (power_cofinality1 icx).
  by rewrite (regular_initial_limit1 omega_limit) (proj2 (regular_omega)).
move: (power_cofinality1 icy).
move: (regular_initial_successor OS0); rewrite succ_o_zero -/omega1.
by move => [pa pb];rewrite - pb (cofinality_card pa)(regular_initial_limit1 la).
Qed.

Lemma ord_sup_aleph x: limit_ordinal x ->
  \csup (range (Lg x \aleph)) = \aleph x.
Proof.
move => lx.
have fgf: fgraph (Lg x \aleph) by fprops.
move: aleph_pr11 => [_ h]; rewrite (h _ lx).
congr (union _ ); set_extens t.
  move /(range_gP fgf) ; bw;move => [z zb]; bw => ->.
  apply /funI_P; ex_tac.
move => /funI_P [z za zb]; apply /(range_gP fgf) ; bw.
ex_tac; bw; ue.
Qed.

Lemma infinite_increasing_power1 X b:
  ofg_Mle_leo X -> domain X = \omega b -> ordinalp b ->
  limit_ordinal (\osup (range X)) ->
  card_prod (Lg (domain X) (fun z => \aleph (Vg X z))) =
  \aleph (\osup (range X)) ^c \aleph b.
Proof.
move => px dx ob la.
set Y := Lg _ _.
have p1: fgraph Y by rewrite /Y; fprops.
have p2: infinite_c (domain Y) by rewrite /Y; bw; rewrite dx; apply aleph_pr5c.
move: (increasing_sup_limit3 px la) => pb.
move: px => [fgx pa xi].
have p3: (forall a : Set, inc a (domain Y) -> \0c <c Vg Y a).
  by rewrite /Y; bw => a adx; bw; apply: aleph_nz1;apply: pa.
have p4: forall u v, inc u (domain Y) -> inc v (domain Y) -> u <=o v ->
    Vg Y u <=c Vg Y v.
  rewrite /Y; bw => u v ud vd uv; bw; apply: aleph_le_lec.
  apply: (xi _ _ ud vd uv).
rewrite (infinite_increasing_power p1 p2 p3 p4).
by rewrite /Y; bw; rewrite pb dx.
Qed.

Lemma infinite_increasing_power2 X b:
  ofg_Mlt_lto X -> domain X = \omega b -> ordinalp b ->
  card_prod (Lg (domain X) (fun z => \aleph (Vg X z))) =
  \aleph (\osup (range X)) ^c \aleph b.
Proof.
move=> p1 p3 p4.
have lb: limit_ordinal (domain X) by rewrite p3; apply: aleph_limit.
move: (increasing_sup_limit2 p1 lb) => la.
move: ( ofg_Mlt_lto_p3 p1 lb) => p2.
by apply: infinite_increasing_power1.
Qed.

Lemma ord_sup_aleph_sum x: ordinalp x ->
  \csup (range (Lg omega0 (fun z=> \aleph (x +o z)))) =
    \aleph (x +o omega0).
Proof.
move => ox.
move: (normal_ofs_compose aleph_pr11 (osum_normal ox)) => [_ xb].
by move: (xb _ omega_limit) => /= ->; rewrite Lg_range.
Qed.

Lemma cprod_inf_eq x y i:
   fgraph x -> fgraph y -> (domain x = domain y) ->
   inc i (domain x) -> (Vg x i) <> \0c -> Vg y i <> \0c ->
   (exists j, [/\ inc j (domain x), j <> i, infinite_c (Vg x j),
     Vg x i <=c Vg x j & Vg y i <=c Vg x j]) ->
   (forall j, inc j (domain x) -> j = i \/ Vg x j = Vg y j) ->
  card_prod x = card_prod y.
Proof.
move => pa pb pc pd pe pf [j [qa qb qc qd qe]] ph.
set x' := Lg (domain x) (fun z => Yo (z = i) (Vg x j) (Vg x z)).
set y' := Lg (domain y) (fun z => Yo (z = i) (Vg y j) (Vg y z)).
have svj: Vg x j = Vg y j by case: (ph _ qa) => // aux; by case: qb.
have sp: x' = y'.
  rewrite /x' /y' -pc; apply: Lg_exten => k kdx; bw; Ytac xeq; Ytac0 => //.
  case: (ph _ kdx) => // aux.
suff: forall z, fgraph z -> inc i (domain z) -> Vg z i <> \0c ->
    inc j (domain z) -> j <> i -> infinite_c (Vg z j) -> Vg z i <=c Vg z j ->
  card_prod z = card_prod (Lg (domain z)(fun t => Yo (t = i)(Vg z j) (Vg z t))).
  move => aux.
  rewrite (aux x pa pd pe qa qb qc qd) -/ x'.
  rewrite pc in pd qa; rewrite svj in qc qe.
  by rewrite (aux y pb pd pf qa qb qc qe) -/ y' sp.
move => z fgz idz jdz znz jni iv jv.
set z1 := (Lg (domain z) (fun t => Yo (t = i) (Vg z j) (Vg z t))).
move: (setC1_K idz); set j1 := (domain z) -s1 i => pA.
symmetry in pA.
have aux1: ~ inc i j1 by move /setC_P => [_] /set1_P; case.
rewrite (induction_prod1 pA aux1).
have fgz1: fgraph z1 by rewrite /z1; fprops.
have pB: domain z1 = j1 +s1 i by rewrite /z1; bw.
rewrite (induction_prod1 pB aux1).
have fg2: fgraph (restr z j1) by fprops.
have fg3: fgraph (restr z1 j1) by fprops.
have pC: sub j1 (domain z) by move => t /setC1_P [].
have pD: sub j1 (domain z1) by rewrite /z1; bw.
have jj: inc j j1 by apply /setC1_P; split => //.
have dr1: (domain (restr z j1)) = j1 by bw.
have dr2: (domain (restr z1 j1)) = j1 by bw.
have jdz1: inc j (domain (restr z j1)) by ue.
move: (setC1_K jdz1); set j2 := _ -s1 j => pE.
symmetry in pE.
have aux2: ~ inc j j2 by move /setC1_P=> [_].
rewrite (induction_prod1 pE aux2).
rewrite dr1 -dr2 in pE.
rewrite (induction_prod1 pE aux2) - cprodA - cprodA.
have sc: sub j2 j1 by move => t /setC1_P []; rewrite dr1.
move: (sub_trans sc pC) => sd.
rewrite (double_restr _ sc) (double_restr _ sc).
rewrite /z1; bw; Ytac0; Ytac0; congr ( (card_prod _ ) *c _).
 apply: fgraph_exten; fprops; bw.
   move=> k kj2.
   have k2: inc k (domain z) by apply: sd.
   by bw;Ytac ki; [ move: (sc _ kj2); rewrite ki |].
by rewrite (product2_infinite jv iv jdz) (square_of_infinite iv).
Qed.

Lemma infinite_prod_pA:
  card_prod (Lg Bnat succ) = card_prod (Lg Bnat (fun z => (succ (succ z)))).
Proof.
set j := Bnat -s1 \0c.
set f := (Lg Bnat succ).
have fgf: fgraph f by rewrite /f; fprops.
have sj:sub j (domain f) by rewrite /f; bw;apply sub_setC.
have sj1: sub (singleton \0c) Bnat by move=> t /set1_P ->; fprops.
have f1: (forall i, inc i ((domain f) -s j) -> (Vg f i) = \1c).
  rewrite /f/j; bw => i /setC_P [iB] /setC_P nv; bw.
  rewrite - succ_zero; ex_middle aux; case: nv;split => //.
  by dneg i0; move /set1_P: i0 => ->.
rewrite (cprod_one_unit sj f1).
set g := Lf succ Bnat j.
have ta: lf_axiom succ Bnat j.
   rewrite /j; move => t tB; apply /setC_P;split;fprops.
   move /set1_P; apply: succ_nz.
have bg: bijection g.
   apply: lf_bijective => //.
     move => u v uB vB;apply: succ_injective1; fprops.
   rewrite /j; move => y /setC_P [yb] /set1_P ynz.
   move: (cpred_pr yb ynz) => [pa pb]; ex_tac.
set X := Lg j (Vg f).
have fgX: fgraph X by rewrite /X; fprops.
have tX: target g = domain X by rewrite /g/X; bw; aw.
have fg: function g by fct_tac.
rewrite /card_prodb (cprod_Cn tX bg); congr (card_prod _).
rewrite /composef /g;aw.
apply: Lg_exten => t tB.
move: (ta _ tB) => aux.
rewrite -/(Vf g t) (lf_V ta tB) /X/f; bw; apply: (BS_succ tB).
Qed.

Lemma infinite_prod_pB: card_prod (Lg Bnat succ) = \2c ^c omega0.
Proof.
move:omega_infinitec => io.
have : card_prod (Lg Bnat succ) <=c card_prod (cst_graph omega0 omega0).
  rewrite /cst_graph; apply: cprod_increasing; bw; fprops.
  move=> x xB; bw; apply: finite_le_infinite => //.
  by apply /BnatP; apply: BS_succ.
rewrite cpow_pr2 (infinite_power1_b io) => le1.
apply: card_leA => //.
rewrite - cpow_pr2.
rewrite infinite_prod_pA.
rewrite /cst_graph;apply: cprod_increasing; bw; fprops.
move=> x xB; bw.
have sxb: inc (succ x) Bnat by fprops.
have cs: cardinalp (succ \0c) by apply: CS_succ.
have cs0: cardinalp (\0c) by fprops.
rewrite - succ_one - succ_zero; apply /(card_le_succ_succP cs); fprops.
move: (CS_Bnat xB) => h.
apply /(card_le_succ_succP CS0 h); apply: (czero_least h).
Qed.

Lemma cprod_An1 a b f: ordinalp a -> ordinalp b ->
  card_prod (Lg (a +o b) f) =
   card_prod (Lg a f) *c card_prod (Lg b (fun z => f (a +o z))).
Proof.
move => oa ob.
set x := Lg b (fun z => f (a +o z)).
set g := Lg (a +o b) f.
have fgg: fgraph g by rewrite /g; fprops.
have sab:= proj33 (osum_Mle0 oa ob).
move: (is_partition_with_complement sab).
have -> : a +o b = domain g by rewrite /g; bw.
move=> pfa.
rewrite (cprod_An pfa).
rewrite /partition_with_complement; bw; symmetry; apply: cprod2_pr.
set ff := fun l: Set => _.
have ->: (card_prod (Lg a f)) = ff C0.
   rewrite /ff /card_prodb /g; bw; apply: f_equal; apply: Lg_exten.
   by move => s sf /=; bw; apply: sab.
suff: (card_prod x) = ff C1 by move => ->; apply doubleton_fam_canon.
rewrite /ff;bw; rewrite /g; bw.
set E := ((a +o b) -s a).
have ba: lf_axiom [eta ord_sum2 a] b E.
  move => t tb; apply/setC_P; rewrite (osum_rec_def oa ob);split.
    apply /setU2_P; right; apply/funI_P; ex_tac.
  move=> /(ord_ltP oa) h1; move:(osum_Mle0 oa (ordinal_hi ob tb)) => tc;ord_tac.
set h := Lf (fun z => a +o z) b E.
have bh: bijection h.
  apply: lf_bijective => //.
    move => u v uo vo su.
    move: (ordinal_hi ob uo) (ordinal_hi ob vo) => ou ov.
    exact (osum2_simpl ou ov oa su).
  by rewrite/E (osum_rec_def oa ob); move => y /setC_P [/setU2_P] [] // /funI_P.
have fh: function h by fct_tac.
have qa: fgraph (Lg E f) by fprops.
have qb: target h = domain (Lg E f) by rewrite /h; bw; aw.
have -> : card_prodb E (Vg (Lg (a +o b) f)) = card_prod (Lg E f).
  congr (card_prod _); apply: Lg_exten=> t /setC_P [ta tb]; bw.
rewrite (cprod_Cn qb bh);rewrite /composef {1} /h {1} /Lf;aw.
congr card_prod; apply: Lg_exten => t to; rewrite -/(Vf h t) /h; aw; bw.
by apply:ba.
Qed.

Lemma infinite_prod_pB1: union (range (Lg Bnat succ)) = omega0.
Proof.
rewrite Lg_range; set_extens t.
  move => /setU_P [z tz /funI_P [u u1 uv]].
  move: tz; rewrite uv (succ_of_Bnat u1) => /setU1_P; case; last by move ->.
  apply: (ordinal_transitive OS_omega u1).
move => tu; apply/setU_P; exists (succ_o t); fprops.
rewrite - (succ_of_Bnat tu); apply /funI_P; ex_tac.
Qed.

Lemma infinite_prod_pB2:
   card_prod (Lg Bnat succ) = \2c ^c omega0.
Proof.
set x := (Lg Bnat succ).
have fgf: fgraph x by rewrite / x; fprops.
have icy: infinite_c (domain x) by rewrite /x; bw; apply: omega_infinitec.
have pa: cardinal_pos_fam x.
  move;rewrite /x; bw; move=> a adx; rewrite /x; bw;apply: succ_positive.
have pb: fg_Mle_lec x.
  move;rewrite /x; bw; move => a b aB bB [_ _ ab]; bw.
  move:(CS_Bnat aB) (CS_Bnat bB) => ca cb.
  apply /(card_le_succ_succP ca cb); split => //.
rewrite (infinite_increasing_power fgf icy pa pb).
rewrite /x infinite_prod_pB1; bw.
rewrite infinite_power1_b //;exact omega_infinitec.
Qed.

Lemma infinite_prod_pC:
   card_prod (Lg Bnat \aleph) = (\aleph omega0) ^c omega0.
Proof.
set x := (Lg Bnat \aleph).
have fgf: fgraph x by rewrite / x; fprops.
have icy: infinite_c (domain x) by rewrite /x; bw; apply: omega_infinitec.
have pa: cardinal_pos_fam x.
  move;rewrite /x; bw; move=> a adx; rewrite /x; bw; apply: aleph_nz1.
  exact (ordinal_hi OS_omega adx).
have pb: fg_Mle_lec x.
  move;rewrite /x; bw; move => a b aB bB ab; bw;exact (aleph_le_lec ab).
rewrite (infinite_increasing_power fgf icy pa pb).
rewrite /x (ord_sup_aleph omega_limit); bw.
Qed.

Lemma infinite_prod_pD (o2 := omega0 +o omega0):
   card_prod (Lg o2 \aleph) = (\aleph o2) ^c omega0.
Proof.
set oo := (\aleph o2).
move: OS_omega => ioo.
apply: card_leA.
  have -> : oo ^c omega0 = oo ^c (omega0 +o omega0).
    by rewrite - cpow_prb cardinal_omega2 cpow_prb.
  have oo2: ordinalp o2 by apply: OS_sum2.
  rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing; bw; fprops.
  by move=> x xB;bw; apply: aleph_le_lec; apply/(ord_leP oo2); apply:setU1_r.
set p1:= card_prod (Lg omega0 (fun z => (\aleph (omega0 +o z)))).
set x := (Lg omega0 (fun z : Set => \aleph (omega0 +o z))).
have fgf: fgraph x by rewrite / x; fprops.
have icy: infinite_c (domain x) by rewrite /x; bw; apply: omega_infinitec.
have pa: cardinal_pos_fam x.
  move;rewrite /x; bw; move=> a adx; rewrite /x; bw; apply: aleph_nz1.
   by apply: OS_sum2 => //; apply(ordinal_hi ioo adx).
have pb: fg_Mle_lec x.
  move;rewrite /x; bw; move => a b aB bB ab; bw.
  exact (aleph_le_lec (osum_Meqle ab ioo)).
move: (infinite_increasing_power fgf icy pa pb).
have ->: union (range x) = oo by apply: (ord_sup_aleph_sum ioo).
rewrite {2} /x; bw; move => <-.
move: (cprod_An1 \aleph ioo ioo).
rewrite -/x -/ o2; move => ->.
have fg1: fgraph (Lg omega0 \aleph) by fprops.
rewrite cprodC; apply: cprod_M1le; rewrite /card_prod;fprops.
apply /cprod_nzP; red;bw => i id; bw; apply: aleph_nz; ord_tac.
Qed.

Lemma infinite_prod_pE (o2 := omega1 +o omega0):
   card_prod (Lg o2 \aleph) = (\aleph o2) ^c aleph1.
Proof.
set o1 := \aleph \1o.
move: omega_infinitec => ico.
move: OS_omega => ioo.
have oo1: ordinalp o1 by apply: OS_aleph; apply: OS1.
move: (aleph_pr5c OS1) => io1.
move /infinite_c_P2: (io1) => io2.
have px: card_prod (Lg o1 \aleph) = (\aleph o1 ^c o1) ^c omega0.
   rewrite - cpow_pow (product2_infinite io2 io1 omega_nz) //.
   set x := (Lg o1 \aleph).
   have qa: (fgraph x) by rewrite /x; fprops.
   have qb: (infinite_c (domain x)) by rewrite /x; bw.
   have qc: cardinal_pos_fam x.
     move; rewrite /x; bw => a ao; bw; apply: aleph_nz1; ord_tac.
   have qd: fg_Mle_lec x.
     move; rewrite /x; bw; move => a b ax bx ab; bw.
     exact (aleph_le_lec ab).
  move: (infinite_increasing_power qa qb qc qd).
  rewrite /x; rewrite (ord_sup_aleph (aleph_limit OS1)); bw.
have pa: card_prod (Lg omega0 (fun z => (\aleph (o1 +o z)))) =
   (\aleph o2) ^c omega0.
   set x := (Lg omega0 (fun z => (\aleph (o1 +o z)))).
   have qa: (fgraph x) by rewrite /x; fprops.
   have qb: (infinite_c (domain x)) by rewrite /x; bw.
   have qc: cardinal_pos_fam x.
     move; rewrite /x; bw => a ao; bw; apply: aleph_nz1.
     by apply: OS_sum2 => //; apply (ordinal_hi ioo ao).
   have qd: fg_Mle_lec x.
     move;rewrite /x; bw; move => a b ax bx ab; bw.
     exact (aleph_le_lec (osum_Meqle ab oo1)).
  move: (infinite_increasing_power qa qb qc qd).
  rewrite /x; move => ->; bw; congr (_ ^c _).
  by rewrite (ord_sup_aleph_sum oo1).
have <- : card_prod
    (Lg omega0 (fun z => (\aleph (o1 +o z) ^c o1))) = \aleph o2 ^c o1.
  move: pa; set f:= Lg omega0 _.
  have pb: fgraph f by rewrite /f; fprops.
  move: (cpow_prod o1 f); rewrite /card_prodb.
  have -> : (Lg (domain f) (fun i => Vg f i ^c o1)) =
    (Lg omega0 (fun z => \aleph (o1 +o z) ^c o1)).
    rewrite /f; bw; apply: Lg_exten => t te; bw.
  move => <- ->.
  rewrite - cpow_pow cprodC (product2_infinite io2 io1 omega_nz) //.
suff: card_prod (Lg omega0 (fun z => \aleph (o1 +o z) ^c o1)) =
  card_prod (Lg omega0 (fun z => \aleph o1 ^c o1 *c \aleph (o1 +o z))).
  move => ->; rewrite -/(card_prodb omega0 _).
  rewrite - prod_of_prods (cprod_An1 \aleph oo1 ioo) /card_prodb cpow_pr2 px //.
set l1:= Lg _ _; set l2 := Lg _ _.
have la: fgraph l1 by rewrite /l1; fprops.
have lb: fgraph l2 by rewrite /l2; fprops.
have lc: (domain l1 = domain l2) by rewrite /l1 /l2; bw.
have ld: inc \0o (domain l1) by rewrite /l1; bw; apply /BnatP; fprops.
have oz: inc \0c omega0 by fprops.
have aux1: \aleph o1 ^c o1 <> \0c.
     apply: infinite_nz; apply: infinite_pow2; apply: aleph_pr5c; fprops.
have le: (Vg l1 \0c) <> \0c by rewrite /l1; bw; rewrite (osum0r oo1).
have lf: (Vg l2 \0c) <> \0c.
  rewrite /l2; bw.
  by rewrite (osum0r oo1); apply: cprod2_nz => //; apply: aleph_nz.
have lg: (exists j, [/\ inc j (domain l1), j <> \0c, infinite_c (Vg l1 j),
     Vg l1 \0o <=c Vg l1 j & Vg l2 \0o <=c Vg l1 j]).
  have oo: inc \1o omega0 by fprops.
  have d1: domain l1 = omega0 by rewrite /l1; bw.
  have i1d: inc \1o (domain l1) by ue.
  have le1: \aleph (o1 +o \0o) <=c \aleph (o1 +o \1o).
    apply: aleph_le_lec;apply: osum_Meqle; try apply: ozero_least; fprops.
  exists \1o; split => //.
  - fprops.
  - rewrite /l1; bw; apply: infinite_pow2; apply: aleph_pr5c; fprops.
  - rewrite /l1; bw; apply: cpow_Mleeq => //.
    apply: aleph_nz; apply: OS_sum2; fprops.
  rewrite /l1/l2; bw.
  rewrite (osum0r oo1).
  set w := \aleph (o1 +o \1o) ^c o1.
  have sa: \aleph o1 <> \0c by apply: aleph_nz; fprops.
  have sb: \aleph o1 ^c o1 <=c w.
      apply: cpow_Mleeq => //; apply: aleph_le_lec.
      apply: osum_Mle0; fprops.
  have sc: \aleph o1 <=c \aleph o1 ^c o1.
     have co1: cardinalp (\aleph o1) by apply CS_aleph.
     apply: cpow_Mle1 => //;apply: aleph_nz => //; fprops.
  move: (ge_infinite_infinite (aleph_pr5c oo1) sc) => i2.
  move: (product2_infinite1 sc i2) => xx; co_tac.
have lh: (forall j, inc j (domain l1) -> j = \0o \/ Vg l1 j = Vg l2 j).
  rewrite /l1 /l2; bw; move => j jb.
  case: (equal_or_not j \0o) => jnz;[by left | right; bw].
  move: (card_card (CS_Bnat jb)) => pd.
  have pb: \aleph \1o <> \0o by apply: aleph_nz; fprops.
  have pc: cardinal j <=c \aleph \1o.
    rewrite pd; apply: (card_leT _ io2).
    by apply: finite_le_infinite => //; apply /BnatP.
  have pe: infinite_c (\aleph (o1 +o j)).
    apply: aleph_pr5c; apply: OS_sum2 => //;apply: (ordinal_hi ioo jb).
  move: (infinite_power5 oo1 (ordinal_hi ioo jb) (CS_aleph OS1) pb pc).
  have ->: \omega (o1 +o j) ^c cardinal j = \omega (o1 +o j) ^c j.
     apply: cpow_pr; fprops.
  by rewrite - /omega1 -/o1 (power_of_infinite pe jb jnz).
by rewrite (cprod_inf_eq la lb lc ld le lf lg lh).
Qed.

Lemma infinite_prod3 X c (Y:= Lg (domain X) (fun z => \aleph (Vg X z)))
   (b:= omega0 ^o c):
   \0o <o c -> ofg_Mlt_lto X -> domain X = b ->
  (card_prod Y) = (\csup (range Y)) ^c (cardinal b).
Proof.
move => cp ax db.
have oc: ordinalp c by ord_tac.
have lb: limit_ordinal b by apply: indecomp_limit2.
move: (lb); rewrite -db => lb1.
move: (increasing_sup_limit4 ax lb1) (aleph_sum_pr6 ax lb1); rewrite -/Y.
set a := \osup (range X); move=> [la sra sav] pa.
move: ax => [gx ofx si]; rewrite sav.
apply: card_leA; first by apply : infinite_increasing_power_bound1 => //.
have pb: \omega a <=c card_prod Y.
   rewrite pa;apply:compare_sum_prod1 => //; rewrite /Y; fprops.
   by bw; move=> i idx; bw; apply:infinite_ge_two; apply: aleph_pr5c;apply: ofx.
move: (cpow_Mleeq (cardinal b) pb (aleph_nz (proj31 la))).
rewrite db;move => h; apply: (card_leT h); clear pa pb h.
have dY: domain Y = b by rewrite /Y; bw.
set f := Lg (coarse b) (fun z => Vg Y (P z)).
have df: domain f = (coarse b) by rewrite /f; bw.
have fgf: fgraph f by rewrite /f; fprops.
have fgY: fgraph Y by rewrite /Y; fprops.
have ->: card_prod Y ^c cardinal b = card_prod f.
  set g := Lg b (fun z => (singleton z) \times b).
  have pa: partition_w_fam g (domain f).
    split => //.
        rewrite /g; fprops.
      red;rewrite /g; bw;move => i j id jd; bw.
      case: (equal_or_not i j) => ij; [ by left | right ].
      apply: disjoint_pr => u /setX_P [_ p1 _] /setX_P [_ p2 _].
      by case: ij; move: p1 p2 => /set1_P <- /set1_P <-.
    rewrite df /coarse /g; set_extens t.
      move /setUb_P; bw; move => [y yb]; bw; move => /setX_P [p1] /set1_P.
      move => p2 p3; apply /setX_P;split => //; ue.
     move => /setX_P [p1 p2 p3]; apply /setUb_P; bw; exists (P t); bw.
     apply /setX_P;split;fprops.
  rewrite (cprod_An pa) (cpow_prod _ Y) dY /g; bw;congr (card_prod _).
  apply: Lg_exten; move => x xb.
  set s:= ((singleton x) \times b).
  have xx: cardinal s = cardinal b.
    apply /card_eqP; eqsym; apply :equipotent_rindexed.
  rewrite - (cpow_pr3 _ xx); congr card_prod.
  have sa: sub s (coarse b).
    move=> t /setX_P [p1 /set1_P p2 p3]; apply /setX_P;split => //; ue.
  have sb: sub s (domain f) by ue.
  have qa: s = domain (restr f s) by bw.
  rewrite /cst_graph; apply: fgraph_exten; [fprops | fprops | bw | bw].
   move => v vd; bw; rewrite /f; bw; last by apply: sa.
   by move: vd => /setX_P [_ /set1_P -> _].
set g := Lg b (fun z => Zo (coarse b) (fun t => (P t) +#o (Q t) =z)).
have pg: partition_w_fam g (domain f).
  split => //; rewrite /g /coarse/mutually_disjoint; bw.
  - fprops.
  - move => i j ib jb; case: (equal_or_not i j) => ij; [ by left | right ].
    bw;apply: disjoint_pr => u /Zo_hi p1 /Zo_hi p2; case: ij.
    by rewrite - p1 - p2.
  - rewrite df /coarse;set_extens t.
      by move /setUb_P; bw; move => [y yb]; bw; move => /Zo_P [].
    move: lb => [ob _ _] tb.
    move: (tb) => /setX_P [pt /(ord_ltP ob) p1 /(ord_ltP ob) p2].
    have pa: inc (ord_natural_sum (P t) (Q t)) b.
      by apply /(ord_ltP ob); apply:ord_natural_small.
    by apply /setUb_P; bw; ex_tac; bw;apply: Zo_i.
rewrite (cprod_An pg).
apply: cprod_increasing; [ rewrite dY /g; bw | bw].
rewrite /g; bw => x xb; bw.
move: (ord_natural_finite_cover oc xb).
rewrite - /b /coarse; set E:= Zo _ _; move => [pa pb].
have dr: domain (restr f E) = E.
  rewrite restr_d //; rewrite /E df; apply: Zo_S.
have xd: inc x (domain X) by ue.
have le1: forall i, inc i E -> Vg f i <=c Vg Y x.
  rewrite /f; move => i => /Zo_P [qa qb]; bw.
  move: qa => /setX_P [_ ipb iqb].
  move: (ordinal_hi (proj31 lb) ipb) => op.
  move: (ordinal_hi (proj31 lb) iqb) => oq.
  move: (ord_natural_M0le op oq); rewrite qb.
  case: (equal_or_not (P i) x) => eq1.
    rewrite eq1 => _; apply: card_leR; rewrite /Y; bw; apply aleph_pr5c.
    by apply: ofx.
   have pd: inc (P i) (domain X) by ue.
  move => eq2; move: (proj1 (si _ _ pd xd (conj eq2 eq1))) => le2.
  by rewrite /Y; bw; apply: aleph_le_lec.
have ix: infinite_c (Vg Y x).
  by rewrite /Y; bw; apply: aleph_pr5c; apply: ofx.
rewrite - (power_of_infinite ix pa pb) - (cpow_pr3 _ (refl_equal (cardinal E))).
apply: cprod_increasing; rewrite /cst_graph ? dr; bw.
by move => t tE; bw; apply: le1.
Qed.

Lemma cardinal_indecomposable2 x: infinite_c x ->
  (exists2 n, \0o <o n & x = omega0 ^o n).
Proof.
move => ix; move: (cardinal_indecomposable ix) => idx.
move: (indecomp_prop3 idx) => [y oy xv]; exists y => //.
move: xv (proj2 (infinite_gt_one ix)).
case: (ord_zero_dichot oy) => // ->; rewrite opowx0 => -> // .
Qed.

Lemma infinite_prod4 X a b
  (Y:= Lg (domain X) (fun z => \aleph (Vg X z) ^c \aleph b))
  (c := \cf a):
  limit_ordinal a -> c <=c \aleph b -> domain X =c ->
  ordinalp b -> ofg_Mlt_lto X -> (a = \osup (range X)) ->
  (card_prod Y) = \aleph a ^c (\aleph b).
Proof.
move => oa ca cdx ob ofx av.
move: (cofinality_limit3 oa); rewrite -/c => lc.
move: (CS_cofinality (proj31 oa)); rewrite -/c => cc.
have icc: infinite_c c by split => //; apply: limit_infinite.
move: (cardinal_indecomposable2 icc) => [n np cv].
rewrite - cdx in cv lc.
move: (infinite_prod3 np ofx cv).
move: (increasing_sup_limit4 ofx lc); rewrite -av; move => [pa _ pc].
rewrite pc - cv cdx (card_card (proj1 icc)) => pd.
move: (f_equal (fun z => z ^c \aleph b) pd).
rewrite - cpow_pow cpow_prod.
have ->: c *c \omega b = \omega b.
  rewrite cprodC; apply: product2_infinite => //.
  by apply: aleph_pr5c.
  by apply: infinite_nz.
move => <-; bw; rewrite /Y; congr (card_prod _).
rewrite cdx;apply Lg_exten; move => x xd /=; bw.
Qed.

Lemma infinite_prod_o1 (X := Lg omega1 id):
  [/\ (exists2 n, \0o <o n & omega1 = omega0 ^o n),
   ofg_Mlt_lto X, domain X = omega1 & (\osup (range X) = omega1)].
Proof.
have ic: (infinite_c omega1) by apply aleph_pr5c; fprops.
move: (proj1 (proj1 ic)) => oo.
rewrite /X;split.
- exact (cardinal_indecomposable2 ic).
- have fhx: fgraph (Lg omega1 id) by fprops.
  split => //; hnf; bw; [ move=> t to; bw;ord_tac0 | move => u v uo vo uv; bw].
- bw.
- rewrite identity_r.
  by move /(limit_ordinal_P1 oo): (infinite_card_limit2 ic) => [_].
Qed.

Lemma infinite_prod_pF:
   card_prod (Lg omega1 \aleph) = (\aleph omega1) ^c aleph1.
Proof.
have ic: (infinite_c omega1) by apply aleph_pr5c; fprops.
move: (proj1 (proj1 ic)) => oo.
move: infinite_prod_o1 => [[n np ov] osf did osx].
rewrite {2} ov in did.
move: (infinite_prod3 np osf did); rewrite did - ov.
move: (indecomp_limit2 np); rewrite {1} ov -did => lo.
move: (increasing_sup_limit4 osf lo).
rewrite did; move=> [pa pb].
rewrite - ov osx; move => ->.
set Y := Lg _ _.
have <-: Y = (Lg omega1 \omega).
    rewrite /Y; bw; apply : Lg_exten => x xo; bw.
rewrite (card_card (proj1 ic)) //.
Qed.

Lemma infinite_prod_pG b: \1o <=o b ->
   card_prod (Lg omega1 (fun z => (\aleph z) ^c (\aleph b)))
   = (\aleph omega1) ^c (\aleph b).
Proof.
have ic: (infinite_c omega1) by apply aleph_pr5c; fprops.
move: (proj1 (proj1 ic)) => oo.
move: infinite_prod_o1 => [[n np nv] osf osx etc] b1.
have oa: ordinalp omega1 by apply: OS_aleph; fprops.
have la: limit_ordinal omega1 by apply: aleph_limit; fprops.
have pa: cofinality omega1 = omega1.
  move: (regular_initial_successor OS0); rewrite succ_o_zero.
  rewrite - (cofinality_card ic); by move => [_ ->].
have pb: cofinality omega1 <=c \omega b.
   by rewrite pa; apply: aleph_le_lec.
have pc: ordinalp b by ord_tac.
rewrite - {2} pa in osx.
rewrite - (infinite_prod4 la pb osx pc osf (sym_eq etc)).
bw; congr (card_prod _); apply: Lg_exten => x xe; bw.
Qed.

Lemma infinite_prod_pH b: ordinalp b ->
   card_prod (Lg omega0 (fun z => (\aleph z) ^c (\aleph b)))
   = (\aleph omega0) ^c (\aleph b).
Proof.
move => b1.
have oa: ordinalp omega0 by fprops.
have la: limit_ordinal omega0 by apply: omega_limit.
have pa: cofinality omega0 = omega0 by move: (regular_omega) => [].
have pb: cofinality omega0 <=c \omega b.
   by rewrite pa - aleph_pr1; apply: aleph_le_lec; apply ozero_least.
set X := Lg omega0 id.
have fhx: fgraph X by rewrite /X;fprops.
have osx: domain X = (cofinality omega0) by rewrite pa /X; bw.
have ofx: ofg_Mlt_lto X.
  rewrite /X; split; fprops.
     hnf; bw; move => t to; bw; ord_tac0.
  red; bw; move => u v uo vo uv; bw.
rewrite - (infinite_prod4 la pb osx b1 ofx).
  apply: f_equal; rewrite /X Lg_domain; apply: Lg_exten => x xb; bw.
rewrite /X identity_r.
by move: la => /(limit_ordinal_P1 oa) [].
Qed.

Lemma infinite_prod5 a:
  (limit_ordinal a) ->
  card_prod (Lg a \aleph) = (\aleph a) ^c (cardinal a).
Proof.
move => la.
pose p j := limit_ordinal j ->
  card_prod (Lg j \omega) = \omega j ^c cardinal j.
apply: (least_ordinal2 (p:=p)) (proj31 la) la => y oy etc ly.
move: (cantor_of_limit ly) => [c [n [oc on nz yv cp]]].
have np : \0o <o n by ord_tac1.
move: (OS_pow OS_omega on) => op.
case: (equal_or_not c \0o) => cz.
  move: yv; rewrite cz (osum0l op) => yv.
  set X := (Lg y id).
  have dx: domain X = omega0 ^o n by rewrite -yv /X; bw.
  have osx: ofg_Mlt_lto X.
    rewrite /X /ofg_Mlt_lto /ordinal_fam; bw;split;fprops.
    red; bw;move => x xy; bw; ord_tac0.
    red; bw;move => u v ux vx uv; bw.
  move: (infinite_prod3 np osx dx).
  have ->: (Lg (domain X) (fun z => \omega (Vg X z))) = (Lg y \omega).
    rewrite /X; bw; apply: Lg_exten => t te; bw.
  by move => ->; rewrite - yv ord_sup_aleph.
case: cp => [ cnz // |[lc le1 sv]].
have cy: c <o y.
  by move: (osum_Meqlt (opow_pos ord_lt_0omega on) oc); rewrite (osum0r oc) -yv.
move: (etc _ cy lc); rewrite - sv => eq1.
rewrite {1} yv (cprod_An1 \aleph oc op) eq1.
set X := Lg (omega0 ^o n) (fun z => (c +o z)).
have dx: domain X = omega0 ^o n by rewrite /X; bw.
have xx: ofg_Mlt_lto X.
  split; rewrite /X; fprops.
      hnf;bw; move => x xv; bw; apply:OS_sum2 => //; ord_tac0.
  red; bw; move => u v ud vd; bw => lt1.
  apply: osum_Meqlt => //; ord_tac0.
move: (infinite_prod3 np xx dx).
set L1:= Lg _ _; set L2 := Lg _ _.
have ->: L1 = L2 by rewrite /L1 /L2 /X; bw; apply: Lg_exten => x xd; bw.
have l1: limit_ordinal (omega0 ^o n) by apply:indecomp_limit2.
have ->: union (range L2) = \omega y.
  move: (normal_ofs_compose aleph_pr11 (osum_normal oc)) => [_ xb].
  by move: (xb _ l1); rewrite -/L2 /= yv; move => ->; rewrite /L2 Lg_range.
move => ->;clear L1 L2.
have cc: cardinalp (cardinal y) by apply: CS_cardinal.
have cnz: cardinal y <> \0c.
  by apply:cardinal_nonemptyset1; move: ly => [_ ok _]; exists \0c.
have le2: cardinal (omega0 ^o n) <=c cardinal y.
  by apply ordinal_cardinal_le1; rewrite yv; apply: osum_M0le.
by move: (infinite_power5 oc op cc cnz le2); rewrite -yv => ->.
Qed.

Lemma infinite_prod6 a:
  ordinalp a -> a <> \0o ->
  card_prod (Lg (succ_o a) \aleph) = (\aleph a) ^c (cardinal a).
Proof.
move => oa anz.
pose p j := j <> \0o ->
  card_prod (Lg (succ_o j) \omega) = \omega j ^c cardinal j.
apply: (least_ordinal2 (p:= p)) oa anz => y oy lyp ynz.
have ->: card_prod (Lg (succ_o y) \aleph) =
    (card_prod (Lg y \omega)) *c (\aleph y).
  rewrite - (ord_succ_pr oy) (cprod_An1 \aleph oy OS1); congr (_ *c _).
  set f := Lg _ _.
  have fg: fgraph f by rewrite /f; fprops.
  have df: domain f = singleton \0o by rewrite /f; bw.
  have f0: Vg f \0o = \omega y.
    rewrite /f; bw; [by rewrite (osum0r oy) | by apply /set1_P ].
  by rewrite (cprod_trivial1 df) // f0; apply: CS_aleph.
have cny: cardinal y <> \0c.
    case: (emptyset_dichot y) => ey; first by contradiction.
    by apply cardinal_nonemptyset1.
case: (limit_ordinal_pr2 oy) => h; first contradiction; last first.
  have onz: \omega y <> \0c by apply: aleph_nz.
  have p1: \omega y <=c \omega y ^c cardinal y.
      apply: (cpow_Mle1 (CS_aleph oy) cny).
  move: (ge_infinite_infinite (aleph_pr5c oy) p1) => p2.
  by rewrite (infinite_prod5 h); apply: (product2_infinite).
move: h => [z oz zv].
case: (equal_or_not z \0o) => znz.
  rewrite zv znz succ_o_zero.
  set f := Lg _ _.
  have fg: fgraph f by rewrite /f; fprops.
  have df: domain f = singleton \0o by rewrite /f; bw.
  have f0: Vg f \0o = \omega \0o.
    by rewrite /f; bw; apply /set1_P.
  have cv: cardinalp (Vg f \0o) by rewrite f0; apply: CS_aleph; fprops.
  rewrite (cprod_trivial1 df cv) f0.
  have p1: \omega \0o <=c \omega \1o.
    by apply: aleph_le_lec; apply: (ozero_least OS1).
  rewrite cprodC (product2_infinite p1 (aleph_pr5c OS1) (aleph_nz OS0)).
  rewrite (card_card CS1) cpowx1 //; co_tac.
have lt1: z <o y by rewrite zv; apply: ord_succ_lt.
rewrite zv in cny.
rewrite zv (lyp _ lt1 znz) (infinite_power2 oz cny); congr (_ *c _).
case: (p_or_not_p (infinite_o z)) => zi.
  red in zi; have <- //: cardinal z = cardinal (succ_o z).
  by apply /card_eqP.
have fz:finite_o z by split.
rewrite - (succ_of_finite fz).
have zB: inc z Bnat by apply /BnatP.
rewrite (card_card (CS_Bnat zB)) (card_card (CS_succ z)).
rewrite (pow_succ _ zB).
symmetry.
have onz: \omega z <> \0c by apply: aleph_nz.
have p1: \omega z <=c \omega z ^c z.
    apply: (cpow_Mle1 (CS_aleph oz) znz).
move: (ge_infinite_infinite (aleph_pr5c oz) p1) => p2.
apply: (product2_infinite) => //.
Qed.

Lemma infinite_power7c x y:
  cardinalp x -> cardinalp y ->
  cardinal (unionb (Lg x (functions y)))
  <=c (card_sum (Lg (cardinals_lt x) (fun z => z ^c y))) *c x.
Proof.
move => cx cy.
set g := Lg _ _.
have fg: fgraph g by rewrite /g; fprops.
apply: (card_leT (csum_pr1 _)).
set f := (Lg x (fun z => cardinal z ^c y)).
have fgf: fgraph f by rewrite /f; fprops.
set h := Lg (cardinals_lt x) (fun i => Zo x (fun t => (cardinal t) = i)).
have fgh: fgraph h by rewrite /h; fprops.
have dh: domain h = (cardinals_lt x) by rewrite /h; bw.
have mh: mutually_disjoint h.
  by apply mutually_disjoint_prop2 => i j z id jd /Zo_hi => <- /Zo_hi <-.
move: (proj1 cx) => ox.
have ph: partition_w_fam h (domain f).
  split => //; rewrite /f; bw; set_extens t.
     move /setUb_P => [z za];rewrite /h; bw ; [by move => /Zo_P [] | ue].
  move => tx; apply /setUb_P.
  have ot: ordinalp t by ord_tac.
  have ts: inc (cardinal t) (cardinals_lt x).
    apply /(cardinals_ltP cx); apply /(ordinal_cardinal_le2P cx ot);ord_tac.
  exists (cardinal t); [by rewrite dh | by rewrite /h;bw; apply: Zo_i].
rewrite /card_sumb;set u := card_sum _.
move: (csum_An ph).
have -> : u = card_sum f.
   rewrite /u /f; apply: f_equal; rewrite /g; bw; apply: Lg_exten=> t tx.
   by bw; rewrite cpow_pr1 (card_card cy).
move ->.
rewrite -dh.
have fgfxx: fgraph (Lg (domain h) (card_pow^~ y)) by fprops.
rewrite cprodC (cprod2_sumDn); bw.
apply: csum_increasing; bw.
move=> z zd; bw.
have pc: sub (Vg h z) (domain f).
  move: ph => [_ _ un]; rewrite -un.
  move=> t th; apply /setUb_P; exists z => //; ue.
have pd: sub (Vg h z) x by move: pc; rewrite /f; bw.
have pb: domain (restr f (Vg h z)) = Vg h z by rewrite restr_d //.
rewrite /card_sumb.
have ->: (Lg (Vg h z) (Vg f)) = Lg (Vg h z) (fun t => z ^c y).
  apply: Lg_exten; fprops; bw.
  rewrite /f => t td; move: (pd _ td) => tx; bw.
   move: td; rewrite /h; bw; [ move /Zo_P; move => [_ -> //] | ue].
rewrite csum_of_same cprodC.
have ->: Vg h z *c z ^c y = cardinal (Vg h z) *c z ^c y.
  by apply cprod2_pr2; fprops; rewrite double_cardinal.
apply cprod_Mlele.
  by move: (sub_smaller pd); rewrite (card_card cx).
apply: card_leR; rewrite /card_pow;fprops.
Qed.

Lemma infinite_power7d x (y := cardinal (cardinals_lt x)):
   cardinalp x -> x <> \0c ->
   (y <=c x /\ y <> \0c).
Proof.
move=> cx xnz; split.
  have pf: sub (cardinals_lt x) x.
    move => t /Zo_P [_ ok]; move: (ordinal_cardinal_lt ok).
    by move =>/ ord_ltP0 [_ _].
  by move: (sub_smaller pf); rewrite (card_card cx).
apply: cardinal_nonemptyset1; exists \0c.
by apply /(cardinals_ltP cx); split; [apply: czero_least | apply:nesym ].
Qed.

Lemma infinite_power7 x y:
  infinite_c x -> y <c \cf x -> y <> \0c ->
  x ^c y = (card_sum (Lg (cardinals_lt x) (fun z => z ^c y))) *c x.
Proof.
move=> pa pb pc.
have cy: cardinalp y by co_tac.
have cx: cardinalp x by move: pa => [].
move: (infinite_power7b pa pb) => le1.
move: (infinite_power7c cx cy) => le2.
apply: card_leA; first by co_tac.
have xnz: x <> \0c by apply: infinite_nz.
have pd: x <=c x ^c y.
  have y1: \1c <=c y by apply: card_ge1.
   apply: cpow_Mle1; fprops.
have ip: infinite_c (x ^c y) by apply: (ge_infinite_infinite pa pd).
apply: product2_infinite4 => //.
set f := (Lg (cardinals_lt x) (card_pow^~ y)).
have fl: (forall i, inc i (domain f) -> Vg f i <=c ( x ^c y)).
  rewrite /f; bw; move=> i id; bw.
  case: (equal_or_not i \0c) => iz.
     rewrite iz (cpow0x pc);apply: czero_least; co_tac.
  move: id => /(cardinals_ltP cx); move => [le _].
  by apply: cpow_Mleeq.
move: (infinite_power7d cx xnz) => [pe1 pf].
have fgf: fgraph f by rewrite /f; fprops.
move: (csum_of_small_b1 (conj fgf fl)); rewrite {2}/f; bw.
rewrite - cprod2_pr2b product2_infinite //; co_tac.
Qed.

Lemma infinite_power7e n y:
  limit_ordinal n -> cardinalp y -> y <> \0c ->
  \aleph n <=c \osup (fun_image n (fun z => (\aleph z) ^c y)).
Proof.
move=> ln yc ynz.
move: aleph_pr11 => [qa qb]; rewrite (qb _ ln).
set T2:= fun_image _ _.
have cst2: cardinal_set T2.
move: (ln) => [on _ _].
move =>t /funI_P [z zn ->]; apply: CS_aleph; ord_tac0.
set T := fun_image _ _.
have csr: cardinal_set T.
  move=> t /funI_P [z zn ->]; rewrite /card_pow; fprops.
apply: (card_ub_sup cst2); first by apply: (CS_sup csr).
move => // a /funI_P [z zn ->].
have sr1: inc ((\aleph z) ^c y) T by apply /funI_P; ex_tac.
apply: card_leT (card_sup_ub csr sr1).
move : (ordinal_hi (proj31 ln) zn) => oz.
by apply: cpow_Mle1; fprops; apply: CS_aleph.
Qed.

Lemma infinite_power7f n y:
  limit_ordinal n -> y <c \cf n ->
  (\aleph n) ^c y = \osup (fun_image n (fun z => (\aleph z) ^c y)).
Proof.
move => p1 p2.
move: (proj31 p1) => on.
case: (equal_or_not y \0c) => yz.
  rewrite yz cpowx0; set T := fun_image _ _.
  suff: T = singleton \1c by move => ->; rewrite setU_1.
  apply set1_pr.
    by move: p1 => [q1 q2 q3]; apply /funI_P; exists \0o => //; rewrite cpowx0.
  by move=> t /funI_P [z zn ->]; rewrite cpowx0.
move: (aleph_pr5c on); set x:= \aleph n => icx.
rewrite - (regular_initial_limit1 p1) in p2.
move: (infinite_power7 icx p2 yz) => aux.
set T := fun_image _ _.
have cst: cardinal_set T by move=> t /funI_P [z _ ->]; fprops.
set s := union T.
have s3: s <=c x ^c y.
   apply: (card_ub_sup cst); first by fprops.
   move => a /funI_P [z zn ->].
   have [zn1 _]: z <o n by apply /ord_ltP.
   have nz: \aleph z <> \0c by apply: aleph_nz; ord_tac.
   by apply: cpow_Mleeq => //; apply: aleph_le_lec.
move: aux; set f := (Lg (cardinals_lt x) (card_pow^~ y)) => aux.
have cff: cardinal_fam f by rewrite /f; hnf; bw; move=> a ad; bw; fprops.
have cx: cardinalp x by move: icx => [].
have cdf1: cardinal (domain f) <=c x.
  rewrite /f; bw; exact (proj1 (infinite_power7d cx (infinite_nz icx))).
have fgf: fgraph f by rewrite /f; fprops.
have osr: ordinal_set (range f).
  move=> t /(range_gP fgf); rewrite /f; bw; move=> [z zv -> ].
  bw;apply: OS_cardinal; fprops.
have sr: s = \osup (range f).
  rewrite /s /T /f; apply: ord_sup_1cofinal => //; split.
    move=> t /funI_P [z zn ->]; apply /(range_gP fgf).
    have os: inc (\aleph z) (cardinals_lt x).
      apply /(cardinals_ltP cx); apply: aleph_lt_ltc.
      by apply /ord_ltP.
    rewrite /f; bw; exists (\aleph z); bw.
  move=> a /(range_gP fgf); rewrite /f; bw; move=> [u us]; bw => ->.
  move: us => /(cardinals_ltP cx) us.
  have cu: cardinalp u by co_tac.
  case: (finite_dichot cu) => fc.
     exists (omega0 ^c y) => //.
       apply /funI_P; exists \0o => //.
         by move: p1 => [_ ].
       by rewrite aleph_pr1.
     apply: ordinal_cardinal_le.
     case: (equal_or_not u \0c) => uz.
       rewrite uz (cpow0x yz); apply: czero_least; rewrite /card_pow;fprops.
     apply: cpow_Mleeq=> //;apply: finite_le_infinite => //.
     apply: (omega_infinitec).
  move:(ord_index_pr1 fc) => [om uv].
  exists (u ^c y).
    apply /funI_P; exists (ord_index u); rewrite ? uv => //.
    apply /(ord_ltP on); apply: aleph_ltc_lt => //; ue.
  apply: ordinal_cardinal_le; apply: card_leR; rewrite /card_pow;fprops.
move: (infinite_power7e p1 (proj31_1 p2) yz).
rewrite -/x -/T -/s => xs.
have pc: (infinite_c s) by apply: (ge_infinite_infinite icx xs).
have pd: cardinal (domain f) <=c s by co_tac.
rewrite sr in pc pd xs.
move: (csum_of_small_b4 fgf cff pc pd); rewrite aux sr; move => ->.
by apply: product2_infinite => //; apply: infinite_nz.
Qed.

Lemma infinite_power7f1 n y:
  limit_ordinal n -> y <c \cf n -> y <> \0c ->
  (\aleph n) ^c y = card_sum (Lg n (fun z => (\aleph z) ^c y)).
Proof.
move => pa pb pc.
move: (infinite_power7f pa pb).
rewrite - Lg_range; set A := union (range _) => h; rewrite h.
have cf: cardinal_fam (Lg n (fun z : Set => \omega z ^c y)).
  by hnf; bw; move=> a an; bw; fprops.
move: (pa) => [on _].
move: (ordinal_cardinal_le1 (aleph_pr6 on)).
rewrite (card_card (CS_aleph on)) => le2.
symmetry; apply: csum_of_small_b4 => //.
    fprops.
  by rewrite -/A -h; apply: infinite_pow => //; apply: aleph_pr5c.
bw; rewrite -/A -h.
apply: (card_leT le2 (cpow_Mle1 (proj32 le2) pc)).
Qed.

Lemma infinite_prod_pI:
  card_sumb omega1 (fun z => \aleph z ^c omega0) = \aleph omega1 ^c omega0.
Proof.
have la: limit_ordinal omega1 by apply: aleph_limit; fprops.
have ic: infinite_c omega1 by apply: aleph_pr5c; fprops.
have cf: omega0 <c cofinality omega1.
    move: (regular_initial_successor OS0) => [_];rewrite succ_o_zero -/ omega1.
  rewrite cofinality_card // => ->.
  rewrite - aleph_pr1; apply: aleph_lt_ltc; apply: ord_lt_01.
rewrite (infinite_power7f1 la cf) //; first by apply: omega_nz.
Qed.

Lemma infinite_power8 n (x:= \aleph n) (z:= \cf x) y:
   ordinalp n -> z <=c y ->
   x ^c y = ( \osup (fun_image (cardinals_lt x) (fun t => t ^c y))) ^c z.
Proof.
move=> ln cy.
set T := fun_image _ _.
have cst: cardinal_set T.
   move=> t /funI_P [zs _ ->]; rewrite /card_pow; fprops.
have icx: infinite_c x by apply: aleph_pr5c.
have cxy: cardinalp (x ^c y) by rewrite /card_pow; fprops.
move: (cofinality_card icx) => H.
move: (cofinality_infinite icx); rewrite H -/z => icz.
move: (ge_infinite_infinite icz cy) => icy.
have sx: \osup T <=c x ^c y.
  apply: (card_ub_sup cst) => //.
  move=> a /funI_P [u up ->].
  case: (equal_or_not u \0c) => uz.
    rewrite uz cpow0x; [by apply czero_least | by apply: infinite_nz].
  apply: cpow_Mleeq => //.
  by move: up => /(cardinals_ltP (proj1 icx)); move => [].
apply: card_leA; last first.
  have znz: z <> \0c by apply: infinite_nz.
  case: (equal_or_not (\osup T) \0c) => snz.
    by rewrite snz cpow0x => //; apply czero_least.
  have : (\osup T) ^c z <=c (x ^c y) ^c z by apply: cpow_Mleeq => //.
  rewrite - cpow_pow (product2_infinite cy) //.
move: (cofinality_c_pr3 icx) => pb.
move: pb => [f [[[pc1 pc2 pd pe] pf] pc]].
have qa: x <=c card_prod f.
   rewrite -pf; apply: compare_sum_prod1 => //.
have : x ^c y <=c (card_prod f) ^c y.
   by apply: cpow_Mleeq => //;apply: infinite_nz.
rewrite (cpow_prod _ f) /card_prodb.
set p := card_prod _.
have: p <=c card_prod (cst_graph (domain f) (\osup T)).
  apply: cprod_increasing; bw.
  bw => t tdf; bw.
    apply: card_sup_ub => //; apply /funI_P; exists (Vg f t) => //.
    by apply /(cardinals_ltP (proj1 icx)); apply: pd.
rewrite cpow_pr2 pe H -/z => le1 le2; co_tac.
Qed.

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.
move => icx icy.
move: (infinite_nz icy) => ynz.
move: (infinite_nz icx) => xnz.
split.
    by move => h; apply: infinite_power1_a => //; apply: infinite_ge_two.
  move=> z le1 le2; apply: card_leA.
    rewrite - {2} (square_of_infinite icy) cpow_pow.
    by apply: cpow_Mleeq.
  have znz: z <> \0c.
    move=> bad; case: xnz; move: le2; rewrite bad cpow0x // => b1.
    apply (card_le0 b1).
  apply: cpow_Mleeq => //; exact (proj1 le1).
move => h.
have x2: \2c <c x by apply: finite_lt_infinite => //; apply /BnatP; fprops.
move: (card_le_ltT (proj1 (cantor (proj1 icy))) (h _ x2)) => yx.
move: (ord_index_pr1 icx) => [on xv].
case: (limit_ordinal_pr2 on) => nz.
    move: yx; have ->: x = omega0 by rewrite -xv nz aleph_pr1.
    move: icy => /infinite_c_P2 icy h1; co_tac.
  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=> le1; co_tac.
  move => _.
  move: (infinite_power2 om ynz).
  move: (h _ (aleph_pr10c om)) => le2.
  have pa: (infinite_c (\aleph (succ_o m))) by apply: aleph_pr5c; ue.
  have pb: \aleph m ^c y <> \0c.
    apply: cpow_nz; by apply: aleph_nz.
  by rewrite cprodC (product2_infinite (proj1 le2) pa pb).
split.
  rewrite -xv (regular_initial_limit1 nz) => yc.
  move: (infinite_power7e nz (proj1 icy) ynz).
  rewrite (infinite_power7f nz yc).
  set T := fun_image _ _; move=> le1.
  apply: card_leA => //.
  have cst: cardinal_set T.
    move => t /funI_P [z _ ->]; rewrite /card_pow; fprops.
  apply: (card_ub_sup cst); first by co_tac.
  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 =>/ord_ltP [].
  apply: (proj1 (h _ aux)).
rewrite -xv; move=> cf1.
have oxne: \aleph (ord_index x) <> \0c by ue.
apply: card_leA; 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.
    apply: czero_least;rewrite /card_pow; fprops.
  apply: infinite_nz; apply:cofinality_infinite_cardinal; ue.
apply: cpow_Mleeq => //.
have cst2: cardinal_set T2.
move => t /funI_P [z zn ->]; rewrite /card_pow; fprops.
apply: (card_ub_sup cst2); first by rewrite xv; co_tac.
move=> a; rewrite /T2 xv => /funI_P [z zi ->].
move: zi => /(cardinals_ltP (proj1 icx)) zi.
exact: (proj1 (h _ zi)).
Qed.

Lemma infinite_power7g x y: infinite_c x -> x <=c y ->
  x ^c y = (card_sum (Lg (cardinals_lt x) (fun z => z ^c y))) *c x.
Proof.
move => icx xy.
have cy: cardinalp y by co_tac.
have icy: infinite_c y by apply: (ge_infinite_infinite icx xy).
have ynz: y <> \0c by apply: infinite_nz.
have x2: \2c <=c x by apply: infinite_ge_two.
rewrite (infinite_power1_a (infinite_ge_two icx) xy icy).
have pa: x <=c \2c ^c y by move: (proj1 (cantor cy)) => le; co_tac.
move: (infinite_power7d (proj1 icx) (infinite_nz icx)) => [pb pc].
have cx: cardinalp x by co_tac.
set f := Lg _ _.
have cf: fgraph f by rewrite /f; fprops.
have pd: infinite_c (\2c ^c y) by apply: (ge_infinite_infinite icx pa).
have fl: forall i, inc i (domain f) -> Vg f i <=c \2c ^c y.
  rewrite /f; bw; move=> i idf; bw.
  move: idf => /(cardinals_ltP cx) idf.
  move: (proj1 (card_lt_leT idf xy)) => p1.
  case: (equal_or_not i \0c) => iz.
    rewrite iz (cpow0x ynz); apply: czero_least; rewrite /card_pow; fprops.
  case: (equal_or_not i \1c) => io.
    rewrite io (cpow1x); apply: finite_le_infinite => //.
    apply /BnatP; fprops.
  have i2: \2c <=c i.
    have ci: cardinalp i by co_tac.
    case: (finite_dichot ci) => iB.
      have b1: inc \1c Bnat by fprops.
      move: iB;rewrite /BnatP => iB.
      rewrite - succ_one; apply/(card_le_succ_ltP _ b1); split; fprops.
      apply: card_ge1 => //.
    by apply: infinite_ge_two.
  rewrite (infinite_power1_a i2 p1 icy).
  apply: card_leR; rewrite /card_pow; fprops.
move: (csum_of_small_b1 (conj cf fl)); rewrite {2} /f; bw.
have -> : (\2c ^c y) *c cardinals_lt x
   = (\2c ^c y) *c cardinal (cardinals_lt x).
   by symmetry;apply cprod2_pr2b.
move: (product2_infinite1 (card_leT pb pa) pd) => le1 le2.
move: (card_leT le2 le1) => le3.
apply:card_leA; last by apply: product2_infinite4.
have xnz: x <> \0c by apply: infinite_nz.
have pe: card_sum f <=c card_sum f *c x.
   apply: cprod_M1le => //; rewrite /card_sum; fprops.
apply: (card_leT _ pe).
have d2: inc \2c (cardinals_lt x).
   apply/(cardinals_ltP cx).
   apply: finite_lt_infinite => //; rewrite /BnatP; fprops.
have ->: \2c ^c y = Vg f \2c by rewrite /f; bw.
apply csum_increasing6; rewrite /f;hnf;bw => t ta; bw; fprops.
Qed.

Lemma infinite_power7h x y:
  regular_cardinal x -> \0c <c y ->
  x ^c y = (card_sum (Lg (cardinals_lt x) (fun z => z ^c y))) *c x.
Proof.
move=> /regular_cardinalP [ic cfx] [[_ cy _] nzy].
have ynz: y <> \0c by apply: nesym.
case: (card_le_to_el (proj1 ic) cy) => xy; last first.
  rewrite - cfx in xy; exact: (infinite_power7 ic xy ynz).
by apply: infinite_power7g.
Qed.

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.
move => h; split.
  exists (\2c ^c y); first by apply: (cantor (proj1 h)).
  rewrite - cpow_pow square_of_infinite //.
move: (ord_index_pr1 h)=> [on yv].
move: (succ_c_pr on); rewrite yv; set z:= succ_c y => zv.
have yz: y <c z by rewrite -yv zv; apply: aleph_pr10c.
have oz: ordinalp z by apply: OS_cardinal; co_tac.
move: (OS_succ on) => osn.
have zp: \aleph z <> z.
  move=> eq; rewrite {2} zv in eq.
  move: (aleph_eq oz osn eq).
  move: (aleph_limit osn); rewrite - zv; move => [la lb lc] zs.
  have nz: inc (ord_index y) z by rewrite zs /succ_o; fprops.
  move: (lc _ nz); rewrite - zs => bad; exact (ordinal_irreflexive oz bad).
move: (normal_ofs_fix aleph_pr11 oz) => tp.
move: (cofinality_least_fp_normal aleph_pr11 zp tp) => cft.
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; ord_tac.
have yt: y <c t.
  apply: (card_lt_leT yz).
  rewrite - (card_card cz) - (card_card ct).
  by apply: ordinal_cardinal_le1.
have ict: infinite_c t by apply: (ge_infinite_infinite h (proj1 yt)).
exists t => //.
move: (power_cofinality (infinite_ge_two ict)) => lt1.
apply: (card_lt_leT lt1).
apply: cpow_Mlele.
    by apply: infinite_nz.
  move: ict => [cat _]; fprops.
by rewrite (cofinality_card ict) cft; apply /infinite_c_P2.
Qed.

Definition cpow_less x y :=
  \csup (fun_image (cardinals_lt y) (fun t => x ^c t)).

Notation "x ^<c y" := (cpow_less x y) (at level 30).

Lemma cpow_less_pr0 x y:
  cardinal_set (fun_image (cardinals_lt y) (fun t => x ^c t)).
Proof. move => t /funI_P [z _ ->]; fprops. Qed.

Lemma cpow_less_alt x y :
  infinite_c y -> \2c <=c x ->
  x ^<c y = card_sum (Lg (cardinals_lt y) (fun t => x ^c t)).
Proof.
move=> icy xy.
rewrite /cpow_less; set E := (cardinals_lt y).
set f := (Lg E [eta card_pow x]).
have cf: cardinal_fam f by rewrite/f;hnf;bw => t te; bw; fprops.
set s:= (union (range f)).
have <-: s = union (fun_image E [eta card_pow x]).
  by rewrite /s Lg_range.
move: (proj1 icy) => cy.
move: (infinite_power7d cy (infinite_nz icy)); rewrite -/E; move => [pw _].
suff aux: y <=c s.
  symmetry; apply: csum_of_small_b4 => //.
     rewrite /f;fprops.
  apply: (ge_infinite_infinite icy aux).
  rewrite {1} /f; bw; co_tac.
have fgf: fgraph f by rewrite /f; fprops.
have csr: cardinal_set (range f).
 move => t /(range_gP fgf); rewrite /f;bw;move => [z ze ->]; bw; fprops.
case: (card_le_to_el cy (CS_sup csr)) => //; rewrite -/s => sy.
move: (cantor (CS_sup csr)); rewrite -/s => aux.
suff: \2c ^c s <=c s by move => l1; co_tac.
have sE: inc s E by apply /(cardinals_ltP cy).
apply: (card_leT (cpow_Mleeq s xy card2_nz)).
apply: card_sup_ub => //; apply /(range_gP fgf).
rewrite /f; bw; exists s; bw; split => //.
Qed.

Lemma cpow_less_pr1 x y: \0c <c x -> cardinalp y -> x ^<c y <=c x ^c y.
Proof.
move=> [[_ cx _] xnz] cy ; apply: card_ub_sup; fprops.
  apply: cpow_less_pr0.
move => t /funI_P [z zy ->]; apply: cpow_Mlele => //.
- by apply:nesym.
- by apply card_leR.
- by move: zy => /cardinals_ltP [].
Qed.

Lemma cpow_less_pr2 x y z: z <c y -> x ^c z <=c (x ^<c y).
Proof.
move=> lt1; apply: card_sup_ub; first by apply: cpow_less_pr0.
apply /funI_P;exists z => //; apply /(cardinals_ltP) => //; co_tac.
Qed.

Lemma cpow_less_pr3 x y: \0c <c x -> inc y Bnat ->
  x ^<c (succ y) = x ^c y.
Proof.
move=> [[_ cx _] xnz] yB.
apply: card_leA; last by apply: cpow_less_pr2; apply: card_lt_succ.
apply: card_ub_sup.
- apply:cpow_less_pr0.
- fprops.
- move => i /funI_P [z zi ->]; apply: cpow_Mlele; fprops.
  have cs: cardinalp (succ y) by apply: CS_succ.
  by move: zi => /(cardinals_ltP cs) /(card_lt_succ_leP yB).
Qed.

Lemma cpow_less_pr4 x y: \0c <c x -> infinite_c y ->
  x ^<c (succ_c y) = x ^c y.
Proof.
move=> [[_ cx _] xnz] yi.
move: (yi) => [cy _].
apply: card_leA; last by (apply: cpow_less_pr2; apply:(succ_c_pr2 cy)).
apply: card_ub_sup.
- apply:cpow_less_pr0.
- fprops.
- move => i /funI_P [z /Zo_hi zi ->]; apply: cpow_Meqle;fprops.
  apply: succ_c_pr4 => //.
Qed.

Lemma CS_cpow_less x y: cardinalp (x ^<c y).
Proof. apply: CS_sup; apply: cpow_less_pr0. Qed.

Lemma cpow_less_compare x: infinite_c x ->
  (x <=c \2c ^<c x /\ \2c ^<c x <=c x ^<c x /\ x ^<c x <=c x ^c x).
Proof.
move => icx; move: (proj1 icx) => cx.
move: (infinite_ge_two icx) => x2.
split.
  move: (@cpow_less_pr0 \2c x) => aux.
  case: (card_le_to_el cx (CS_cpow_less \2c x)) => // pa.
  set u := \2c ^<c x.
  have le : \2c ^c u <=c u.
     apply: card_sup_ub => //; apply /funI_P;exists u => //.
     apply /cardinals_ltP =>//; co_tac.
  move: (cantor (proj31_1 pa)); rewrite -/u => lt; co_tac.
split.
  apply: card_sup_image; move=> t tx; apply: cpow_Mleeq.
    by apply: infinite_ge_two.
  fprops.
apply: cpow_less_pr1 => //; split; first by apply: czero_least.
exact: (nesym (infinite_nz icx)).
Qed.

Lemma cpow_less_pr5a x y: cardinalp x -> \2c <=c y -> x <=c x ^<c y.
Proof.
move=> cx y2.
move: (cpow_less_pr2 x (card_lt_leT (card_lt_12) y2)).
by rewrite cpowx1.
Qed.

Lemma cpow_less_pr5b x y: infinite_c x -> \2c <=c y -> infinite_c (x ^<c y).
Proof.
move=> cx y2; apply: (ge_infinite_infinite cx (cpow_less_pr5a (proj1 cx) y2)).
Qed.

Lemma cpow_less_pr5c x: \2c <=c x -> finite_c x -> x ^<c omega0 = omega0.
Proof.
move => x2 xf.
move: CS_omega => co.
move: (@cpow_less_pr0 x omega0) => aux.
move: omega_infinitec => oic.
have xb: inc x Bnat by apply /BnatP.
have le1: x ^<c omega0 <=c omega0.
  apply: card_ub_sup => // i /funI_P [z zx ->].
  move: zx => /(cardinals_ltP co) zx.
  apply: finite_le_infinite => //; apply /BnatP; apply BS_pow; fprops.
  by move: (ordinal_cardinal_lt zx) =>/ord_ltP0 [_ _].
ex_middle neq1.
set t := x ^<c omega0.
have to: t <c omega0 by split.
move: (cpow_less_pr2 x to); rewrite -/t => pa.
move: (cantor (proj31_1 to)) => pb.
move: (card_lt_leT pb (cpow_Mleeq t x2 card2_nz)) => pc; co_tac.
Qed.

Lemma cpow_less_pr5d : \2c ^<c omega0 = omega0.
Proof.
apply: cpow_less_pr5c finite_2; apply: (card_leR CS2).
Qed.

Lemma cpow_less_pr5e x: infinite_c x -> x ^<c omega0 = x.
Proof.
move => icx; move: (proj1 icx) => cx.
move: (cpow_less_pr5a cx (infinite_ge_two omega_infinitec)) => pa.
apply: card_leA; last by exact.
apply: card_ub_sup => //; first by apply: cpow_less_pr0.
move=> i /funI_P [z za ->]; move: za.
move /(cardinals_ltP CS_omega) => za.
move: (ordinal_cardinal_lt za) => /ord_ltP0; move=> [_ _ xn].
by apply: power_of_infinite1.
Qed.

Lemma cpow_less_pr5f (x := omega0): x ^<c x = x.
Proof. by apply: cpow_less_pr5e; apply: omega_infinitec. Qed.

Lemma cpow_less_pr6 x z: infinite_c x -> \2c <=c z ->
  z ^c x = (z ^<c x ) ^c (\cf x).
Proof.
move => icx t2.
move: (cofinality_c_pr3 icx) => [f [ [[pa1 pa2 pb pc] pd] _]].
apply: card_leA.
  rewrite - (cofinality_card icx) -{1} pd (cpow_sum _ f).
  rewrite - pc - cpow_pr2 /cst_graph; bw.
  apply: cprod_increasing; fprops; bw => t td; bw.
  by apply: cpow_less_pr2; apply: pb.
have tp: \0c <c z by exact (card_lt_leT card_lt_02 t2).
move: (cpow_less_pr1 tp (proj1 icx)) => h.
move: (infinite_nz (cofinality_infinite_cardinal icx)) => cnz.
case: (equal_or_not (z ^<c x) \0c).
  move=> ->; rewrite cpow0x //; by apply: czero_least; fprops.
move => aux; move: (cpow_Mleeq (\cf x) h aux).
move: (cofinality_small icx) => cg.
rewrite - cpow_pow (product2_infinite cg icx cnz) //.
Qed.

Lemma cpow_less_pr6a x: infinite_c x ->
  \2c ^c x = (\2c ^<c x ) ^c (\cf x).
Proof.
move => icx; apply: cpow_less_pr6 => //; fprops.
Qed.

Lemma cpow_less_pr7a x: infinite_c x ->
  card_sum (Lg (cardinals_le x) (fun t => x ^c t)) = \2c ^c x.
Proof.
move => icx; move: (icx) => [cx _].
set f := (Lg (cardinals_le x) [eta card_pow x]).
set a := cardinals_lt x.
move: (cardinals_ltP cx) => h1P.
have h2P: forall b, inc b (cardinals_le x) <-> b <=c x.
 move => b; apply /(cardinals_leP cx).
have fgf: fgraph f by rewrite /f; fprops.
have pa: (a +s1 x) = (domain f).
   rewrite /f /a; bw; set_extens t.
     case/setU1_P. move /h1P => aux;apply /h2P; co_tac.
     move => ->; apply /h2P; fprops.
   move /h2P=> aux; apply /setU1_P; case:(equal_or_not t x) => tx; [by right |].
   by left ; apply /h1P; split.
have pb: sub (a +s1 x) (domain f) by rewrite pa; fprops.
have pc: ~(inc x a) by move /h1P => [_].
move: (induction_sum0 f pc).
rewrite pa (restr_to_domain fgf (@sub_refl f)); move => ->.
have pd : inc x (cardinals_le x) by apply/ h2P; fprops.
have ->: (restr f a) = Lg a [eta card_pow x].
  have ax: sub a (cardinals_le x).
    by move: pa; rewrite /f; bw; move => <-; fprops.
  have dr: domain (restr (Lg (cardinals_le x) [eta card_pow x]) a) = a.
     rewrite /f restr_d=> //; bw.
  rewrite /f; apply: fgraph_exten; bw; fprops; fprops.
  by move => t ta /=; bw; apply: ax.
rewrite - (cpow_less_alt icx (infinite_ge_two icx)).
move: (cpow_less_compare icx) => [_ [_ pe]].
rewrite /f; bw; rewrite- (infinite_power1_b icx).
rewrite csumC (sum2_infinite pe) //; apply: infinite_pow => //.
by apply: infinite_nz.
Qed.

Lemma cpow_less_pr7b x (y := succ_c x) : infinite_c x ->
  card_sum (Lg (cardinals_lt y) (fun t => y ^c t)) = \2c ^c x.
Proof.
move => icx; move: (icx) => [cx _].
move:(succ_c_pr2 cx) => pa.
have iy: infinite_c y by apply: (ge_infinite_infinite icx (proj1 pa)).
have y2: \2c <=c y by apply infinite_ge_two.
rewrite - (cpow_less_alt iy y2).
have qa: \0c <c y by move: card_lt_02 => h; co_tac.
by rewrite (cpow_less_pr4 qa icx) infinite_power1 //; apply: succ_c_pr3.
Qed.

Lemma cpow_less_pr8 x:
   infinite_c x -> (forall y, y<c x -> \2c ^c y <c x) ->
   [/\ \2c ^c x = gimel_fct x,
     x <c (\cf (gimel_fct x)) &
     (\cf x = omega0 -> \2c ^c x = x ^c omega0)].
Proof.
move => icx h.
move: (icx) => [cx _].
have pa: \2c ^c x = gimel_fct x.
  rewrite (cpow_less_pr6a icx).
  have le1 : (\2c ^<c x) <=c x.
    apply: card_ub_sup; [apply: cpow_less_pr0 |exact cx | ].
    move =>i /funI_P [z] /(cardinals_ltP cx) pa.
    move => ->; apply: (proj1 (h _ pa)).
  move: (cpow_less_compare icx) => [le2 _].
  by rewrite (card_leA le1 le2).
split; first by exact.
   by rewrite -pa; apply: power_cofinality2.
by rewrite pa /gimel_fct => ->.
Qed.

Lemma cpow_less_pr9 x (y := succ_c x):
  infinite_c x -> ( y ^<c y = \2c ^c x /\ \2c ^<c y = \2c ^c x).
Proof.
move => icx; move: (icx) => [cx _].
have sp: \0c <c succ_c x.
  move: (czero_least cx) (succ_c_pr2 cx) => sa sb; co_tac.
rewrite (cpow_less_pr4 card_lt_02 icx) (cpow_less_pr4 sp icx).
by rewrite (infinite_power1_c icx).
Qed.

Definition cpow_less_ecb x :=
 (exists2 a, a <c x & forall b, a <=c b -> b <c x -> \2c ^c a = \2c ^c b).

Lemma cpow_less_pr10 x: singular_cardinal x -> (cpow_less_ecb x)
  -> \2c ^c x = \2c ^<c x.
Proof.
move => [icx sx] [a ax ha].
move: (cofinality_card icx) => H.
move: (cofinality_small icx) => cg.
have [c [ac cf cx]]: exists c, [/\ a <=c c, \cf x <=c c& c <c x].
  have ca: cardinalp a by co_tac.
  have cx: cardinalp (\cf x) by co_tac.
  case: (card_le_to_ee ca cx) => h.
    exists (\cf x); split; fprops; split; fprops.
  exists a; split;fprops.
have p2: (\2c ^<c x) = \2c ^c c.
  apply: card_leA; last by apply: (cpow_less_pr2 \2c cx).
  apply: card_ub_sup.
      apply: cpow_less_pr0.
    fprops.
  move=> i /funI_P [z zi ->].
  move: zi => /(cardinals_ltP (proj1 icx)) => zx.
  case: (card_le_to_ee (proj31_1 zx) (proj31_1 cx)) => zc.
    apply: cpow_Mlele ; fprops.
  rewrite - (ha _ (card_leT ac zc) zx).
   apply: cpow_Mlele ; fprops.
move: (cpow_less_pr6a icx).
move: (cofinality_infinite icx); rewrite H => coi.
move: (infinite_nz coi) => cnz.
rewrite p2 - cpow_pow product2_infinite//; apply (ge_infinite_infinite coi cf).
Qed.

Lemma gimel_prop n (x:= \aleph n): ordinalp n ->
 [/\ (n = \0c -> \2c ^c x = gimel_fct x),
    (succ_op n) -> \2c ^c x = gimel_fct x,
    (limit_ordinal n -> cpow_less_ecb x ->
       \2c ^c x = \2c ^<c x *c gimel_fct x)&
    (limit_ordinal n -> not (cpow_less_ecb x) ->
       \2c ^c x = gimel_fct (\2c ^<c x))].
Proof.
move => on.
have res1: n = \0c -> \2c ^c x = gimel_fct x.
   move => h; apply: gimel_prop1.
   by rewrite /x h aleph_pr1; apply: regular_cardinal_omega.
have res2: succ_op n -> \2c ^c x = gimel_fct x.
  move => [m om nm].
  move: (regular_initial_successor om); rewrite -nm;apply: gimel_prop1.
move: (aleph_pr5c on); rewrite -/x => icx.
move: (cofinality_infinite_cardinal icx)(gimel_prop2 icx)(icx) => coi g2 [cx _].
have pa: limit_ordinal n -> infinite_c (\2c ^<c x).
  move => ln.
  move: (cpow_less_pr2 \2c (aleph_lt_ltc (limit_positive ln))) => h.
  move: (infinite_powerset (aleph_pr5c OS0)) => ip2o.
  exact (ge_infinite_infinite ip2o h).
split => //.
  move=> ln cs; move: (infinite_powerset icx) => ip2x.
  case: (equal_or_not x (\cf x)) => xcx.
     have rx: regular_cardinal x by apply /regular_cardinalP.
     rewrite - (gimel_prop1 rx) cprodC; symmetry; apply product2_infinite => //.
       apply: cpow_less_pr1 => //; apply: card_lt_02.
     exact (infinite_nz (pa ln)).
  have si: singular_cardinal x by split => //; apply:nesym.
  rewrite - (cpow_less_pr10 si cs).
  symmetry; apply product2_infinite => //.
  apply: infinite_nz; apply: infinite_pow2 => //.
move => ln nl.
move: (pa ln) => paln.
rewrite /gimel_fct (cpow_less_pr6a icx).
suff aux: \cf (\2c ^<c x) = \cf x by ue.
have ox: ordinalp x by apply: OS_cardinal.
have oy: ordinalp (\2c ^<c x) by move: paln => [pb _]; apply: OS_cardinal.
move: (cofinality_rw ox) (cofinality_rw oy) => [qa qb qc] [qd qe qf].
have x1: forall t, t <c x -> \2c ^c t <c \2c ^<c x.
  move => t tx; split; first by apply: cpow_less_pr2.
  move => ub; case: nl; exists t => //.
  move => b b1 b2.
  move: (cpow_M2le b1) (cpow_less_pr2 \2c b2); rewrite - ub.
  move => r1 r2; co_tac.
have x2: forall t, t <o \2c ^<c x -> exists2 u, t <=o \2c ^c u & u <c x.
  move => t tl.
  have ot: ordinalp t by ord_tac.
  move: tl =>/(ordinal_cardinal_le2P (proj1 paln) ot) => tl.
  case: (ord_le_to_el OS_omega ot) => cto; last first.
    exists omega0.
      move: (ordinal_cardinal_lt (cantor CS_omega)) => [le1 _].
      move: cto => [cto _]; ord_tac.
    rewrite - aleph_pr1; apply: aleph_lt_ltc.
    by move: ln => [_ ok _]; apply /ord_ltP.
  move: (infinite_set_pr3 cto) => ict.
  move: (succ_c_pr1 (proj1 ict)) => []; set st := succ_c (cardinal t).
  move=> sa sc sb; move: (sb _ tl) => sd.
  set sst:= Yo (cardinalp t) t st.
  have pc: t <=o sst.
     rewrite /sst; Ytac ct; first by apply: ord_leR.
     case: (ord_le_to_ee ot (proj1 sa)) => // xx.
     move: (ordinal_cardinal_le1 xx); rewrite -/st (card_card sa) => h; co_tac.
  have sdd : sst <c \2c ^<c x.
    rewrite /sst; Ytac ct; first by rewrite - (card_card ct).
    split; [by apply: sd | move => bad ].
    case: (p_or_not_p (exists2 u, u <c x & \2c ^c u = \2c ^<c x)) => H.
      by move: H => [u ua ub]; move: (x1 _ ua) => [_ xbad].
    have bad2: forall w, w <c x -> \2c ^c w <=c (cardinal t).
      move=> w wc;apply: (succ_c_pr4 (proj1 ict)); rewrite -/st bad; split.
        exact: (cpow_less_pr2 \2c wc).
      by move => eq; case: H; exists w.
    have bad3: \2c ^<c x <=c cardinal t.
      apply: card_ub_sup; [ apply: cpow_less_pr0 | apply: CS_cardinal | ].
      by move=> i /funI_P [z zs ->]; apply: bad2; apply /(cardinals_ltP cx).
  move: (card_leT sd bad3) =>bad4; co_tac.
  suff: (exists2 u, sst <=c \2c ^c u & u <c x).
    move => [u /ordinal_cardinal_le p1 p2]; exists u => //; ord_tac.
  ex_middle bad.
  suff b1: \2c ^<c x <=c sst by co_tac.
  apply: card_ub_sup; [by apply: (cpow_less_pr0) | co_tac |].
  move =>i /funI_P [z /(cardinals_ltP cx) zx ->].
  have cs: cardinalp sst by co_tac.
  have c2: cardinalp (\2c ^c z) by fprops.
  by case: (card_le_to_ee cs c2) => // le4; case: bad; exists z.
apply: ord_leA.
  move: (qb) => [f [[ff sf tf] cf]].
  set g := Lf (fun z => \2c ^c (Vf f z)) (\cf x) (\2c ^<c x).
  have ta: lf_axiom (fun z => \2c ^c (Vf f z)) (\cf x) (\2c ^<c x).
    rewrite - sf; move => t ts /=; rewrite - cpow_prb.
    set zz := cardinal _.
    have zzx: zz <c x by apply:cardinal_ordinal_lt1=> //;rewrite -tf; fprops.
    move: (cpow_less_pr2 \2c zzx) => [a1 a2 a3].
    case: (ordinal_sub (OS_cardinal a1) (OS_cardinal a2) a3) => // eq1.
    by move: (x1 _ zzx); rewrite eq1; move => [_ neq].
  have fg: function g by apply: lf_function.
  apply: (qf _ qa); exists g.
  split; [ by red; rewrite /g; split => //; aw | move => t tp].
  have tl: t <o (\2c ^<c x) by apply/ord_ltP.
  move: (x2 _ tl) => [u u1 u2].
  have ui: inc u x by move: (ordinal_cardinal_lt u2) => /ord_ltP0 [_ _].
  move: (cf _ ui) => [z zx le2]; exists z => //.
  rewrite /g; aw.
  move: (ordinal_cardinal_le1 le2) => le3.
  move: (cpow_M2le le3); rewrite cpow_prb cpow_prb.
  move => le4; move: (ordinal_cardinal_le le4) => le5; ord_tac.
move: (qe) => [f [[ff sf tf] cf]].
pose g t := choose (fun u => (Vf f t <o \2c ^c u /\ u <c x)).
have gp: forall t, inc t (source f)-> (Vf f t <o \2c ^c (g t) /\ (g t) <c x).
   move => t /(Vf_target ff); rewrite tf => xx.
   have [sa _ sc]:= (infinite_card_limit2 paln).
   move/(ord_ltP sa): (sc _ xx) => /x2 [u /ord_succ_ltP aux ux].
   by apply choose_pr; exists u.
set G:= Lf g (cofinality (\2c ^<c x)) x.
have ta: lf_axiom g (cofinality (\2c ^<c x)) x.
  move => t; rewrite - sf => stf; move: (gp _ stf) => [_].
  by move /ordinal_cardinal_lt =>/(ord_ltP0) [_ _].
apply: qc => //; exists G; split.
  by rewrite /G; red; aw;split => //; apply: lf_function.
move=> t tx; ex_middle bad.
have pb: forall z, inc z (cofinality (\2c ^<c x)) -> Vf G z <o t.
  move => z zsf; move: (zsf); rewrite - sf => zt.
  have ow: ordinalp (Vf G z).
    rewrite /G; aw; move: (gp _ zt) => [_ xx]; apply: OS_cardinal; co_tac.
  case: (ord_le_to_el (ordinal_hi ox tx) ow) => // yy; case: bad; ex_tac.
have pc: forall z, inc z (cofinality (\2c ^<c x)) -> Vf f z <o \2c ^c t.
  move => z zc;move: (zc); rewrite - sf => /gp [lt1 _].
  move: (pb _ zc); rewrite /G; aw; move => [] /ordinal_cardinal_le1 /cpow_M2le.
  rewrite cpow_prb cpow_prb => /ordinal_cardinal_le x6 _; ord_tac.
have bad2: inc (\2c ^c t) (\2c ^<c x).
  have: (\2c ^c t) <c (\2c ^<c x).
  have -> : (\2c ^c t = \2c ^c (cardinal t)) by apply: cpow_pr; fprops.
  move: (ordinal_hi ox tx) => ot.
  by apply: x1 ; apply /(ordinal_cardinal_le2P cx ot); apply /ord_ltP.
  by move => x3; move: (ordinal_cardinal_lt x3); move/(ord_ltP oy).
move: (cf _ bad2) => [z zc le]; move: (pc _ zc) => le1; ord_tac.
Qed.

Lemma gimel_prop3 x: infinite_c x ->
  [/\ (regular_cardinal x -> \2c ^c x = gimel_fct x),
      (singular_cardinal x -> cpow_less_ecb x -> \2c ^c x = \2c ^<c x) &
     (singular_cardinal x -> not (cpow_less_ecb x) ->
     \2c ^c x = gimel_fct (\2c ^<c x))].
Proof.
move => icx.
move: (ord_index_pr1 icx); set n := (ord_index x); move => [pa pb].
have qa: singular_cardinal x -> limit_ordinal n.
  by rewrite - pb; apply: singular_limit.
move: (gimel_prop pa) => [pc pd pe pf].
rewrite pb in pe pf.
split; first by apply: gimel_prop1.
   by move => qb qc; rewrite cpow_less_pr10.
by move => qb qc; by exact (pf (qa qb) qc).
Qed.

Definition cpow_less_ec_prop x y a:=
  a <c y /\ forall b, a<=c b -> b <c y -> x ^c a = x ^c b.

Lemma cpow_less_ec_pr0 x y:
  infinite_c y -> \2c <=c x -> infinite_c (x ^<c y).
Proof.
move => icy x2.
have pa: forall n, inc n Bnat -> n <=c x ^<c y.
  move => n nB; apply (card_leT (proj1 (cantor (CS_Bnat nB)))).
  move: nB => /BnatP nB.
  apply: card_leT _ (cpow_less_pr2 x (finite_lt_infinite nB icy)).
  by apply: cpow_Mleeq => //; apply: card2_nz.
suff h: omega0 <=c (x ^<c y) by apply: (ge_infinite_infinite omega_infinitec h).
rewrite omega_limit0; apply: card_ub_sup => //.
   by move => t to; apply: CS_Bnat.
move: (pa _ BS2) => aux; co_tac.
Qed.

Lemma cpow_less_ec_pr1 x y:
  cardinalp y -> exists a, cpow_less_ec_prop x (succ_c y) a.
Proof.
move=> cy.
exists y; split; first by move: (succ_c_pr1 cy) => [_ pb _].
move => b yb /(succ_c_pr4 cy) bs; by rewrite (card_leA bs yb).
Qed.

Lemma card_ge2_nz x: \2c <=c x -> x <> \0c.
Proof.
move => x2.
by move: (card_lt_leT card_lt_02 x2) => [_]; apply:nesym.
Qed.

Lemma cpow_less_ec_pr2 x y a:
  cpow_less_ec_prop x y a -> \2c <=c x ->
  forall b, a<=c b -> b <c y -> x ^<c y = x ^c b.
Proof.
move =>[ay h] x2 b le1 le2.
have xnz := (card_ge2_nz x2).
apply: card_leA; last by apply: cpow_less_pr2.
have cy: cardinalp y by co_tac.
apply: card_ub_sup; [ apply: cpow_less_pr0 | fprops | ].
move => i /funI_P [z /(cardinals_ltP cy) lt1 ->].
case: (card_le_to_ee (proj31 le1) (proj31_1 lt1)) => az.
  rewrite - (h _ az lt1) (h _ le1 le2).
  apply: (card_leR); fprops.
exact (cpow_Meqle xnz (card_leT az le1)).
Qed.

Lemma cpow_less_ec_pr3 x y a:
  cpow_less_ec_prop x y a -> \2c <=c x -> singular_cardinal y ->
   (x ^<c y = x ^c a /\ x ^<c y = x ^c y).
Proof.
move => h x2 [icy sy]; move: (h) => [ay h0].
move: (cpow_less_ec_pr2 h x2) => h1.
move: (proj31_1 ay) => ca.
rewrite (h1 _ (card_leR ca) ay).
split; first by exact.
move: (cofinality_small icy) => cg.
have [c [ac cf cx]]: exists c, [/\ a <=c c, \cf y <=c c &c <c y].
  have cx: cardinalp (\cf y) by co_tac.
  case: (card_le_to_ee ca cx) => cp; last by exists a; split;fprops.
  exists (\cf y); split => //; split; fprops.
move: (cofinality_infinite_cardinal icy) => coi.
move: (infinite_nz coi) => cnz.
move: (ge_infinite_infinite coi cf) => icc.
rewrite (cpow_less_pr6 icy x2) (h1 _ ac cx) - cpow_pow.
by rewrite (product2_infinite cf icc cnz) (h0 _ ac cx).
Qed.

Lemma cpow_less_ec_pr4 x y:
  infinite_c y -> \2c <=c x ->
  (exists a, cpow_less_ec_prop x y a) ->
  y <=c \cf (x ^<c y).
Proof.
move => icy x2 [a ha].
move: (cpow_less_ec_pr2 ha x2) => hb.
move: (ord_index_pr1 icy); set i := ord_index y; move=> [oi yv].
have xnz: \0c <c x by apply: card_lt_leT card_lt_02 x2.
case: (limit_ordinal_pr2 oi) => li.
    have yo: y = omega0 by rewrite -yv li aleph_pr1.
    move: ha => [ay h1].
    rewrite (hb _ (card_leR (proj31_1 ay)) ay).
    move: (ordinal_cardinal_lt ay); rewrite yo => /olt_omegaP aB.
    move: (BS_succ aB) => sB.
    have sy: (succ a) <c y.
      rewrite yo; apply: finite_lt_infinite => //; first by apply /BnatP.
      apply: omega_infinitec.
    move: (h1 _ (card_le_succ aB) sy) => eq1.
    case: (finite_dichot (proj32 x2)) => icx.
      have xB: inc x Bnat by apply /BnatP.
      have x1: \1c <c x by exact:(card_lt_leT (card_lt_12) x2).
      by move: (cpow_Mlelt xB sB (card_lt_succ aB) x1) => [_ bad]; case: bad.
    move: (cofinality_infinite_cardinal (infinite_pow icx (@succ_nz a))) => pa.
    by rewrite eq1;apply /infinite_c_P2.
  move: li => [j oj jv].
  have ->: y = succ_c (\aleph j) by rewrite -yv jv succ_c_pr.
  move: (aleph_pr5c oj) => ipy.
  rewrite (cpow_less_pr4 xnz ipy).
  by move: (power_cofinality5 x2 ipy)(succ_c_pr1 (proj1 ipy)) => s [_ _]; apply.
rewrite -yv.
rewrite {1} (proj2 (aleph_pr11) _ li).
move: (ha) => [ay _]; move: (ay) => [[ca _] _ _].
have aa: a <=c a by fprops.
have [c [ic ac cy]]: exists c, [/\ infinite_c c, a <=c c & c <c y].
  case: (finite_dichot ca); last by exists a.
  move: omega_infinitec => io.
  move => fa; exists omega0; split => //; first by apply: finite_le_infinite.
  rewrite - aleph_pr1 -yv; apply: aleph_lt_ltc.
  by move: li => [ori zi _]; apply/ord_ltP.
rewrite yv (hb _ ac cy).
apply: card_ub_sup.
     move => t /funI_P [z zi ->]; apply: CS_aleph; ord_tac0.
   apply: CS_cofinality; exact: (proj1 (CS_pow x c)).
move => t /funI_P [z zi ->].
have zi1: z <o i by move: zi => /ord_ltP [].
move: (aleph_lt_ltc zi1); rewrite yv => lt.
move: (ic) => [cc _].
case: (card_le_to_el cc (proj31_1 lt)) => le1.
  rewrite - (hb _ ac cy) (hb _ (card_leT ac le1) lt).
  apply: (proj1 (power_cofinality5 x2 (aleph_pr5c (proj31_1 zi1)))).
exact:(card_leT (proj1 le1) (proj1 (power_cofinality5 x2 ic))).
Qed.

Lemma cpow_less_ec_pr5 x y:
  infinite_c y -> \2c <=c x ->
  ~ (exists a, cpow_less_ec_prop x y a) ->
  exists X, let Y := Lg (domain X) (fun z => x ^c (Vg X z)) in
    [/\ domain X = \cf y,
     (forall i, inc i (domain X) -> Vg X i <c y),
     (forall i, inc i (domain X) -> Vg Y i <c x ^<c y),
     (y <> omega0 -> card_nz_fam X) &
     \csup (range Y) = x ^<c y ].
Proof.
move => icy x2 ha.
move: (ord_index_pr1 icy); set c := ord_index y; move => [oc yv].
case: (equal_or_not c \0c)=> cz.
  have yo: y = omega0 by rewrite -yv cz aleph_pr1.
  move: omega_infinitec => oic.
  case: (finite_dichot (proj32 x2)) => fcx; last first.
    case: ha; rewrite yo;exists \1c; split; first by apply /clt_omegaP; fprops.
    move => b b1 bo.
    have bnz: b <> \0c by move/card_ge1P:b1 => [_ /nesym].
    by rewrite(cpowx1 (proj1 fcx)) (power_of_infinite fcx) //;apply /clt_omegaP.
  exists (Lg y id); simpl; rewrite yo; split => //.
  - bw.
  - by rewrite (proj2 (regular_omega)).
  - by hnf;bw;move => a ay; bw; apply/clt_omegaP.
  - bw => i ib; bw; rewrite (cpow_less_pr5c x2 fcx); apply/clt_omegaP; fprops.
  - bw; rewrite /cpow_less Lg_range; congr union.
    set_extens t;move /funI_P => [z zo ->]; apply/funI_P.
      exists z; bw;by apply/(cardinals_ltP CS_omega); apply/clt_omegaP.
    move /(cardinals_ltP CS_omega): zo => /clt_omegaP zb; ex_tac; bw.
case: (limit_ordinal_pr2 oc) => // lc.
  move: lc => [d od dv]; case: ha; exists (\aleph d).
  move: (aleph_pr5c od) => ipy.
  move: (succ_c_pr1 (proj1 ipy)) => [pb pc pd].
  move: (succ_c_pr od); rewrite -dv yv => <-; split => //.
  move => b l1 /(succ_c_pr4 (proj1 ipy)) pe; co_tac.
have xnz:= (card_ge2_nz x2).
have pa: 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: ha; 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).
move: (regular_initial_limit1 lc) => cfy.
move: (cofinality_pr4 (proj31 lc)); rewrite - cfy yv; move=> [f fa qe].
move: fa; set cy := \cf y; move => [[[ff sf tf]] cff [_ nf nf1]].
set X := Lg cy (fun z => \aleph (Vf f z)).
have fap: forall z, inc z cy -> inc (Vf f z) c.
  by move => z zx; rewrite -tf; Wtac.
have faq: forall z, inc z cy -> ordinalp (Vf f z).
   move=> z zx; move: (fap _ zx) => wc; ord_tac.
have pb: cardinal_fam X.
  by rewrite /X;hnf;bw; move => a ay; bw;apply: CS_aleph; apply: faq.
have pc: fg_Mlt_ltc X.
  red; rewrite /X; bw;move => a b ac bc ab; bw;apply: aleph_lt_ltc.
  by apply: nf.
have pb': fgraph X by rewrite /X; fprops.
have pd: cardinal_set (range X).
  by move => t /(range_gP pb') [z zd ->]; apply: pb.
have pe: \osup (range X) = y.
  set S := \osup (range X); move: (proj1 icy) => ccy.
  case: (card_le_to_el ccy (CS_sup pd)) => pr1.
    apply:card_leA => //; apply: card_ub_sup=> // i /(range_gP pb').
    rewrite /X; bw; move => [z zy ->]; bw; move /(ord_ltP oc): (fap _ zy) => [].
    by rewrite - yv => /aleph_le_lec.
  have [ra rb rc]: limit_ordinal cy.
    apply: infinite_card_limit2.
    by rewrite /cy - yv cfy; apply: cofinality_infinite_limit.
  have: infinite_c S.
     have: inc (\aleph (Vf f \0c)) (range X).
       apply /(range_gP pb'); rewrite /X; bw; ex_tac; bw.
     move /(card_sup_ub pd); apply: ge_infinite_infinite; apply: aleph_pr5c.
     by apply: faq.
  move/ord_index_pr1 => []; set s := ord_index S => os sv.
  move: pr1; rewrite - /S - sv - yv; move /(aleph_ltc_lt os oc).
  move: lc => [_ c0 cl]; move => /(ord_ltP oc) /cl /cff [z zc h].
  have: inc (\aleph (Vf f z)) (range X).
     apply /(range_gP pb'); rewrite /X; bw; ex_tac; bw.
  move/(card_sup_ub pd); rewrite -/S - sv; move /(aleph_lec_le(proj32 h) os).
  move /ord_lt_succP => h'; ord_tac.
have pi : card_nz_fam X.
  by rewrite /X; hnf; bw; move => i idx; bw; apply: aleph_nz; apply: faq.
have ph: (forall i, inc i (domain X) -> Vg X i <c y).
  rewrite /X; bw; move => i ic;bw. rewrite -yv.
  apply: aleph_lt_ltc; move: (fap _ ic).
  by move /(ord_ltP oc).
set Y := (Lg (domain X) (fun z => x ^c (Vg X z))).
have pf: forall i, inc i (domain X) -> Vg Y i <c x ^<c y.
  move => i idx; rewrite /Y; bw.
  move: (ph _ idx) => /pa [b [ba /(cpow_less_pr2 x) bb bc]]; co_tac.
have pg: union (range Y) = x ^<c y.
  have rb: fgraph Y by rewrite /Y;fprops.
  have ra:cardinal_set (range Y).
    move => t/ (range_gP rb); rewrite /Y; bw; move => [u ud ->]; bw; fprops.
  have rc: cardinalp (x ^<c y) by apply: CS_cpow_less.
  have rd: cardinalp (union (range Y)) by apply: CS_sup.
  move: (@cpow_less_pr0 x y) => re.
  rewrite /Y; bw.
  apply: card_leA.
    apply: card_ub_sup => // i /(range_gP rb).
    by move=> [z]; rewrite {1}/ Y; bw => /pf [] h _ ->.
  apply: card_ub_sup => // i /funI_P [z].
  move /(cardinals_ltP (proj1 icy)) => rf ->.
  have [t tr xt]: exists2 t, inc t (range X) & z <=c t.
     ex_middle bad.
     have yz: y <=c z.
       rewrite -pe; apply : card_ub_sup => //; first by co_tac.
       move => j jr; case: (card_le_to_ee (pd _ jr) (proj31_1 rf)) => //.
       move => zj; case: bad; ex_tac.
     co_tac.
  apply: (card_leT (cpow_Meqle xnz xt)).
  have fgx:fgraph X by rewrite /X; fprops.
  move: tr => /(range_gP fgx) [v va ->].
  apply: card_sup_ub => //; apply /(range_gP rb); bw.
  exists v; bw => //; rewrite /Y; bw.
exists X; split => //; rewrite /X; bw.
Qed.

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.
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: card_leA; last first.
  move: q5; set v := range _ => e1.
  have h: sub v (x ^<c y).
     move => t /(range_gP fgY); bw; move => [z /q3 h ->].
     by move :(ordinal_cardinal_lt h) => /(ord_ltP oz).
  move: (cofinality_pr8 oz h e1).
  move: (range_smaller_cardinal fgY); rewrite -/v q1; bw.
  rewrite (card_card (CS_cofinality (proj1 (proj1 pa)))) => l1 l2; co_tac.
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 /(ord_ltP oz) la: inc (Vf f i) (x ^<c y) by rewrite - tf; Wtac.
  have ou: ordinalp (Vf f i) by ord_tac.
  move/(ordinal_cardinal_le2P cz ou): la => lb.
  move:pa => [cy _]; move: (cy) => [oy _].
  move: (card_lt_sup (@cpow_less_pr0 x y) lb) => [v /funI_P[w]].
  move /(cardinals_ltP cy)=> /ordinal_cardinal_lt => rb -> rc.
  by exists w; split => //; apply /(ord_ltP 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).
move:(proj1 (proj1 pa)) => oy.
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 move: (cofinality_pr8 oy sgy ugy) => p1 p2; co_tac.
have osy: ordinal_set y by move => t/(ordinal_hi oy).
have ->: y = union y.
 by move: (infinite_card_limit2 pa) => /(limit_ordinal_P1 oy) [].
apply: (ord_sup_1cofinal) => //; split => // a /(ord_ltP oy) lay.
have oa: ordinalp a by ord_tac.
move /(ordinal_cardinal_le2P (proj1 pa) oa): lay => /ra [b [sa sb sc]].
have: inc (x ^c b) (x ^<c y).
   apply /(ord_ltP oz); move: (ra _ sb) => [b' [b1 b2 b3]].
   move: (card_lt_leT b3 (cpow_less_pr2 x b2)).
   apply: ordinal_cardinal_lt.
rewrite - sf in cff; move /cff => [c c1 /ordinal_cardinal_le1 c2].
exists (g c); first by apply/funI_P; ex_tac.
move/gp: c1 => [sd se].
move: (card_leT c2 se); rewrite (card_card (CS_pow x b)) => sg.
case: (ord_le_to_ee oa (ordinal_hi oy sd)) => //.
move /ordinal_cardinal_le1 => /(cpow_Meqle xnz); rewrite cpow_prb => l3.
by move: (card_lt_leT sc (card_leT sg l3)) => [].
Qed.

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.
move => icy x2.
move: (cpow_less_ec_pr0 icy x2) => ia.
move: (ia) => [ca _].
have aux: forall z, infinite_c z -> \cf z <=c z.
  move =>t icz;move: (icz) => [cz _]; move:(cz) => [oz _].
  apply: ordinal_cardinal_le3 => //; 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/card_ge1P:z1 => [_ /nesym].
    move :(cpow_less_ec_pr2 ha x2) => hb.
    move: (card_lt_leT z2 cfys) => pb.
    move: (z2) => [[cz _] _ _].
    rewrite /p.
    case: (finite_dichot cz) => fz.
      have zb: inc z Bnat by apply /BnatP.
      by rewrite (power_of_infinite ia zb znz).
    have [b [b1 b2 b3]]: exists b, [/\ a <=c b, z <=c b & b <c y].
      move: ha => [ay _]; move: (ay) => [[ca1 _] _ _].
      case: (card_le_to_ee ca1 cz) => le1.
        by exists z; split => //; apply: card_leR.
      exists a; split;fprops.
    move: (ge_infinite_infinite fz b2) => ib.
    by rewrite /p (hb _ b1 b3) - cpow_pow (product2_infinite b2 ib znz).
  - move => pa pb.
    have sy: singular_cardinal y.
      by split => //; move: (card_le_ltT pa pb) => [_].
    move: (cpow_less_ec_pr3 ha x2 sy) => [pc pd].
    rewrite /p pd - cpow_pow (product2_infinite (proj1 pb) icy) //.
    move: (cofinality_infinite_cardinal icy) => i1.
    exact: (infinite_nz (ge_infinite_infinite 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: (finite_lt_infinite finite_1 icy).
       move: card_le_01 ; rewrite - az => ab.
       rewrite /p (hb _ ab y1) cpowx1 //; co_tac.
     rewrite /p (hb _ (card_leR oa) ay) - cpow_pow (cprodC).
     move: (ge_infinite_infinite icy yz) => iz.
     by rewrite (product2_infinite (card_leT (proj1 ay) yz) iz az).
move => ha.
move: (cpow_less_ec_pr6 icy x2 ha) => hb.
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;bw;move => t td; bw; fprops.
have q10: card_sum 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; bw; 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/card_ge1P:z1 => [_ /nesym].
  rewrite /p (infinite_power7 ia zcy znz).
  set T := Lg _ _.
  have pa: (forall i, inc i (domain T) -> Vg T i <=c x ^<c y).
     rewrite /T; bw => i id; bw.
     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: (card_lt_sup csr le2); move => [v ].
     move /(range_gP fgY); rewrite /Y;bw; move => [w wdx ->]; bw => le3.
     case: (equal_or_not i \0c) => iz.
       rewrite iz (cpow0x znz); apply: (czero_least ca).
     move: (cpow_Mleeq z le3 iz); rewrite - (cpow_pow) => pb.
     apply (card_leT pb); apply: (cpow_less_pr2).
     move: (q2 _ wdx) => le1.
     rewrite hb in zcy; move: (card_lt_leT zcy cfys) => le4.
     by apply: product2_infinite5.
  have ct: cardinal_fam T by rewrite /T; hnf;bw; move => a ad;bw; fprops.
  have ct': fgraph T by rewrite /T; fprops.
  have dt: domain T = cardinals_lt (x ^<c y) by rewrite /T; bw.
  move: (csum_of_small_b1 (conj ct' pa)).
  rewrite dt - cprod2_pr2b.
  move: (infinite_power7d ca (infinite_nz ia)).
  set t := cardinal _; move=> [le2 tnz].
  have snz: card_sum T <> \0c.
    have zt: inc \1c (domain T).
      rewrite /T; bw; apply /(cardinals_ltP ca).
      apply: (finite_lt_infinite finite_1 ia).
    move: (csum_increasing6 ct zt).
    move: zt; rewrite {1}/T; bw => zt;rewrite {1} /T; bw.
    by rewrite cpow1x; move/card_ge1P => [_ /nesym].
  rewrite (product2_infinite le2 ia tnz) => le3.
  by rewrite cprodC (product2_infinite le3 ia snz).
case: (equal_or_not y omega0) => yo.
  split => //.
    move:regular_omega => [ra rb];rewrite yo rb => l1 l2; co_tac.
  move => yz;rewrite /p yo.
  move: omega_infinitec => oic.
  move: (finite_le_infinite finite_2 oic) => o2.
  rewrite yo in yz.
  have icz: infinite_c z by apply: (ge_infinite_infinite oic yz).
  case: (finite_dichot (proj32 x2)) => fx.
    rewrite (cpow_less_pr5c x2 fx).
    rewrite (infinite_power1_a o2 yz icz).
    by rewrite (infinite_power1_a x2 (finite_le_infinite 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 (card_sum (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; bw => i idx; bw.
    move: (q4 yo _ idx) => enz.
    have cx: cardinalp x by co_tac.
    exact (card_leT x2 (cpow_Mle1 cx enz)).
  move: (compare_sum_prod1 pb) => le1.
  have le0: card_sum Y <> \0c by rewrite q10; apply: infinite_nz.
  apply: (card_leT (cpow_Mleeq w le1 le0)).
  rewrite (cpow_prod _ Y) cpow_sum /Y.
  rewrite /card_prodb.
  rewrite Lg_domain Lg_domain; set f1 := Lg _ _; set f2 := Lg _ _.
  have ->: f1 = f2 by apply: Lg_exten => t te; bw; rewrite - cpow_pow.
  apply: card_leR; rewrite /card_prod; fprops.
move: (cofinality_infinite_cardinal icy) => cyi.
split => //.
  move => p1 p2.
  have icz: (infinite_c z) by apply: (ge_infinite_infinite cyi p1).
  move: (pa _ icz); set f := Lg _ _ => pb.
  have pc: card_sum f <=c y.
    have df: domain f = \cf y by rewrite /f; bw; ue.
    have cf0: fgraph f by rewrite /f; fprops.
    have cf2: (forall i, inc i (domain f) -> Vg f i <=c y).
      rewrite /f; bw => i idx; bw; rewrite cprodC.
      apply: (product2_infinite4 (proj1 p2) (proj1 (q2 _ idx)) icy).
    move: (csum_of_small_b1 (conj cf0 cf2)).
    by rewrite df (product2_infinite cfys icy (infinite_nz cyi)).
  apply:card_leA; first by apply: (card_leT 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: (ge_infinite_infinite icy p1).
move: (pa _ icz); set f := Lg _ _ => p2.
have pb: x ^c card_sum 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; bw => i idx; bw; rewrite cprodC.
    apply: product2_infinite1 => //.
    exact (card_leT (proj1 (q2 _ idx)) p1).
  have df: domain f = \cf y by rewrite /f; bw; ue.
  move: (csum_of_small_b1 (conj cf1 cf2)); rewrite df.
  move: (card_leT cfys p1) => le2.
  move: (product2_infinite1 le2 icz) => le3 le4; co_tac.
rewrite /p; apply: card_leA; first by co_tac.
move: (cpow_less_pr5a (proj32 x2) (infinite_ge_two icy)) => le2.
exact: (cpow_Mleeq z le2 xnz).
Qed.