Library sset15

Theory of Sets : Ordinals

Copyright INRIA (2011-2013) Marelle Team (Jose Grimm).


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) \