Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset9.


Module InfiniteSets.

Lemma infinite_Bnat: infinite_set Bnat.
Proof. by case (finite_dichot1 Bnat) => // fs; elim Bnat_infinite. Qed.

Definition induction_defined s a:= choose(fun f=>
  source f = Bnat & surjection f & W 0c f = a &
  forall n, inc n Bnat -> W (succ n) f = s (W n f)).

Definition induction_defined1 h a p := choose(fun f=>
  source f = Bnat & surjection f & W 0c f = a &
  (forall n, n <c p -> W (succ n) f = h n (W n f)) &
  (forall n, inc n Bnat -> ~ (n <=c p) -> W n f = a)).

Definition induction_defined_set s a E:= choose(fun f=>
  is_function f &source f = Bnat & target f = E & W 0c f = a &
  forall n, inc n Bnat -> W (succ n) f = s (W n f)).

Definition induction_defined0_set h a E:= choose(fun f=>
  is_function f & source f = Bnat & target f = E & W 0c f = a &
  forall n, inc n Bnat -> W (succ n) f = h n (W n f)).

Definition induction_defined1_set h a p E := choose(fun f=>
  is_function f &source f = Bnat & target f = E & W 0c f = a &
  (forall n, cardinal_lt n p -> W (succ n) f = h n (W n f)) &
  (forall n, inc n Bnat -> ~ (cardinal_le n p) -> W n f = a)).

Lemma integer_induction1: forall h a p, inc p Bnat ->
  exists_unique (fun f=> source f = Bnat & surjection f &
    W 0c f = a &
     (forall n, cardinal_lt n p -> W (succ n) f = h n (W n f))&
     (forall n, inc n Bnat -> ~ (cardinal_le n p) -> W n f = a)).
Proof.
move=> h a p pB; split.
set (h1:= fun n x => Yo (cardinal_lt n p) (h n x) a).
move: (integer_induction0 h1 a) => [[f [sf [sjf [f0 fn]]]] _].
exists f; ee.
    move => n np; rewrite fn; [rewrite /h1 Y_if_rw // | Bnat_tac].
  move => n nB np.
  have nnz: (n <> 0c) by dneg nz; rewrite nz; fprops.
  move: (predc_pr nB nnz) => [pnB nsp].
  by rewrite nsp (fn _ pnB) /h1 Y_if_not_rw // - lt_n_succ_le//- nsp.
move=> x y [sx [sjx [x0 [xs xl]]]][sy [sjy [y0 [ys yl]]]].
apply function_exten4=>//; first by ue.
rewrite sx; apply cardinal_c_induction; first by ue.
move=> n nB eq.
case (p_or_not_p (n <c p)) => np.
  by rewrite (xs _ np) (ys _ np) eq.
have snp: (~ (succ n) <=c p) by srw; fprops.
move: (BS_succ nB) => snB.
by rewrite (xl _ snB snp) (yl _ snB snp).
Qed.

Lemma induction_defined_pr: forall s a,
  let f := induction_defined s a in
     source f = Bnat & surjection f & W 0c f = a &
     forall n, inc n Bnat -> W (succ n) f = s (W n f).
Proof.
move=> s a f.
rewrite /f/induction_defined.
move: (integer_induction s a)=> [e _].
apply choose_pr=> //.
Qed.

Lemma induction_defined_pr1: forall h a p,
  let f := induction_defined1 h a p in
    inc p Bnat ->
    ( source f = Bnat & surjection f &
      W 0c f = a &
      (forall n, n <c p -> W (succ n) f = h n (W n f))&
      (forall n, inc n Bnat -> ~ (n <=c p) -> W n f = a)).
Proof.
move=> h a p f pB.
rewrite /f/induction_defined1.
move: (integer_induction1 h a pB)=> [e _].
apply choose_pr=> //.
Qed.

Lemma integer_induction_stable: forall E g a,
  inc a E -> (forall x, inc x E -> inc (g x) E) ->
  sub (target (induction_defined g a)) E.
Proof.
move=> E g a eA agE.
move:(induction_defined_pr g a) => [sf [sjf [f0 fn]]] t tt.
move:(surjective_pr2 sjf tt) => [x [xsf]] <-; rewrite sf in xsf.
move: x xsf;apply cardinal_c_induction; first by ue.
by move=> n nB WE; rewrite fn //; apply agE.
Qed.

Lemma integer_induction_stable0: forall E h a,
  inc a E -> (forall n x, inc x E -> inc n Bnat -> inc (h n x) E) ->
  sub (target (induction_defined0 h a)) E.
Proof.
move=> E h a aE ahE.
move:(induction_defined_pr0 h a) => [sf [sjf [f0 fn]]] t tt.
move:(surjective_pr2 sjf tt) => [x [xsf]] <-; rewrite sf in xsf.
move: x xsf;apply cardinal_c_induction; first by ue.
by move=> n nB WE; rewrite fn //; apply ahE.
Qed.

Lemma integer_induction_stable1: forall E h a p,
  inc p Bnat ->
  inc a E -> (forall n x, inc x E -> cardinal_lt n p -> inc (h n x) E) ->
  sub (target (induction_defined1 h a p)) E.
Proof.
move=> E h a p pB aE ahE.
move:(induction_defined_pr1 h a pB) => [sf [sjf [f0 [fs lf]]]] t tt.
move:(surjective_pr2 sjf tt) => [x [xsf]] <-; rewrite sf in xsf.
move: x xsf;apply cardinal_c_induction; first by ue.
move=> n nB WE.
case (p_or_not_p (n <c p)) => np.
  rewrite fs //; apply ahE =>//.
have nsp: ~ cardinal_le (succ n) p by srw; fprops.
rewrite lf //; hprops.
Qed.

Lemma induction_defined_pr_set: forall E g a,
  let f := induction_defined_set g a E in
    inc a E -> (forall x, inc x E -> inc (g x) E) ->
     (is_function f & source f = Bnat & target f = E & W 0c f = a &
     forall n, inc n Bnat -> W (succ n) f = g (W n f)).
Proof.
move=> E g a f aE ag.
rewrite /f/induction_defined_set; apply choose_pr.
move: (induction_defined_pr g a) => [sf [[fjf sjf] [f0 fn]]].
set (h:= corresp Bnat E (graph (induction_defined g a))).
have fh:(is_function h).
  rewrite /h; apply is_function_pr; [fprops | idtac | aw;ue].
  apply sub_trans with (target (induction_defined g a)).
    apply f_range_graph =>//.
  apply integer_induction_stable =>//.
exists h.
rewrite /h/W; rewrite corresp_source corresp_target corresp_graph ; ee.
Qed.

Lemma induction_defined_pr_set0: forall E h a,
  let f := induction_defined0_set h a E in
    inc a E -> (forall n x, inc x E -> inc n Bnat -> inc (h n x) E) ->
     (is_function f & source f = Bnat & target f = E & W 0c f = a &
     forall n, inc n Bnat -> W (succ n) f = h n (W n f)).
Proof.
move=> E g a f aE ag.
rewrite /f/induction_defined0_set; apply choose_pr.
move: (induction_defined_pr0 g a) => [sf [[fjf sjf] [f0 fn]]].
set (h:= corresp Bnat E (graph (induction_defined0 g a))).
have fh:(is_function h).
  rewrite /h; apply is_function_pr; [fprops | idtac | aw;ue].
  apply sub_trans with (target (induction_defined0 g a)).
    apply f_range_graph =>//.
  apply integer_induction_stable0 =>//.
exists h;rewrite /h/W corresp_source corresp_target corresp_graph ; ee.
Qed.

Lemma induction_defined_pr_set1: forall E h a p,
  let f := induction_defined1_set h a p E in
    inc p Bnat ->
    inc a E -> (forall n x, inc x E -> n <c p -> inc (h n x) E) ->
    (is_function f & source f = Bnat & target f = E & W 0c f = a &
      (forall n, n <c p -> W (succ n) f = h n (W n f))&
      (forall n, inc n Bnat -> ~ (n <=c p) -> W n f = a)).
Proof.
move=> E g a p f pB aE ag.
rewrite /f/induction_defined1_set; apply choose_pr.
move: (induction_defined_pr1 g a pB) => [sf [[fjf sjf] [f0 [fs fl]]]].
set (h:= corresp Bnat E (graph (induction_defined1 g a p))).
have fh:(is_function h).
  rewrite /h; apply is_function_pr; [fprops | idtac | aw;ue].
  apply sub_trans with (target (induction_defined1 g a p)).
    apply f_range_graph =>//.
  apply integer_induction_stable1 =>//.
exists h;rewrite /h/W corresp_source corresp_target corresp_graph ; ee.
Qed.

Lemma infinite_greater_countable1: forall E,
  infinite_set E -> (cardinal Bnat) <=c (cardinal E).
Proof.
move=> E iE; red;ee.
rewrite /Bnat (cardinal_of_cardinal omega0_cardinal) -omega0_pr1 //.
apply cardinal_ordinal; fprops.
Qed.

Lemma infinite_greater_countable: forall E,
  infinite_set E -> exists F, sub F E & cardinal F = cardinal Bnat.
Proof.
move=> E ise.
move: (infinite_greater_countable1 ise).
rewrite - cardinal_le_aux2; fprops.
rewrite - eq_subset_card; move=> [F [fe ef]]; exists F;ee; symmetry; aw.
Qed.

Lemma equipotent_N2_N: (product Bnat Bnat) \Eq Bnat.
Proof.
set g2 := fun a => (binom (succ a) 2c).
set mi:= fun n m => n +c (g2 (n +c m)).
have g2B: forall a, inc a Bnat -> inc (g2 a) Bnat.
   rewrite /g2=> a aB; apply BS_binom =>//; hprops.
have miB: forall n m, inc n Bnat -> inc m Bnat -> inc (mi n m) Bnat.
  by move=> n m nB mB; rewrite /mi; hprops.
have ha: forall n m, inc n Bnat -> inc m Bnat ->
    (g2 (n +c m)) <=c (mi n m).
  move=> n m nB mB; rewrite /mi.
  set t:= (g2 (n +c m)).
  rewrite card_plusC; apply (Bsum_increasing3 (g2B _ (BS_plus nB mB)) nB).
have hc: forall n, inc n Bnat-> g2 (succ n) = (g2 n) +c (succ n).
  by move=> n nB; rewrite /g2 (binom_2plus0 (BS_succ nB)).
have hb: forall n m, inc n Bnat -> inc m Bnat ->
  (mi n m) <c (g2 (succ (n +c m))).
  move=> n m nB mB.
  move: (BS_plus nB mB) => sB.
  rewrite (hc _ sB) /mi.
  set t:= (g2 (card_plus n m)).
  have aux: inc t Bnat by rewrite /t; apply g2B; fprops.
  rewrite card_plusC; apply (finite_sum2_lt aux nB aux (BS_succ sB)); fprops.
  srw; apply Bsum_increasing3; fprops.
exists (BL (fun z => (mi (P z) (Q z))) (product Bnat Bnat) Bnat).
rewrite bl_source bl_target; ee;apply bl_bijective.
  move => t; rewrite product_inc_rw; move=> [_ [pB qB]]; intuition.
  move=> u v;rewrite !product_inc_rw; move=> [pu [puB quB]][pv [pvB qvB]] sm.
  have ss: card_plus (P u) (Q u) = card_plus (P v) (Q v).
    move: (ha _ _ puB quB)(hb _ _ puB quB)(ha _ _ pvB qvB)(hb _ _ pvB qvB).
    rewrite sm; move=> r1 r2 r3 r4.
    move: (cardinal_le_lt_trans r1 r4)(cardinal_le_lt_trans r3 r2)=> r5 r6.
    have gi: forall x y, inc x Bnat -> inc y Bnat ->
      (g2 x) <c (g2 (succ y)) -> x <=c y.
      have ls2: forall z, inc z Bnat -> 2c <=c (succ (succ z)).
        move => z zB; rewrite -succ_one -(lt_n_succ_le1 cardinal1 (BS_succ zB)).
        rewrite -succ_zero; rewrite -(lt_n_succ_le1 cardinal0 zB); fprops.
      have n2z: 2c <> 0c by apply card_two_not_zero.
      move=> x y xB yB; rewrite /g2.
      rewrite - (binom_monotone2 inc2_Bnat (BS_succ xB) (BS_succ (BS_succ yB)) n2z).
      rewrite (lt_is_le_succ _ (BS_succ yB)) - lt_n_succ_le1; fprops.
      fprops.
    move : (BS_succ yB)=> h;fprops.
    move: (BS_plus puB quB) (BS_plus pvB qvB) => sun svn.
    apply (cardinal_antisymmetry1 (gi _ _ sun svn r5)(gi _ _ svn sun r6)).
  move: sm; rewrite /mi ss; set (w:= g2 (card_plus (P v) (Q v))).
  have wB: inc w Bnat by apply (g2B _ (BS_plus pvB qvB)).
  move=> ss2; move: (plus_simplifiable_right wB puB pvB ss2) => sp.
  rewrite sp in ss; apply (pair_exten pu pv sp).
  apply (plus_simplifiable_left pvB quB qvB ss).
move=> y yB.
have g2z: g2 0c = 0c.
  rewrite /g2 succ_zero (binom_bad inc1_Bnat inc2_Bnat) //.
  rewrite -succ_one; apply (is_lt_succ inc1_Bnat).
  fprops.
case (equal_or_not y 0c) => yz.
  rewrite yz; exists (J 0c 0c).
  move: inc0_Bnat => bz.
  split; [fprops | rewrite pr1_pair pr2_pair].
  by rewrite /mi (Bnat0_unit_suml bz) g2z (Bnat0_unit_suml bz).
set (p:= fun k=> inc k Bnat & cardinal_lt y (g2 k)).
have pa: forall k, p k -> inc k Bnat by move=> k [kB _].
have pb: (~ p 0c).
  rewrite /p g2z; move=> [_ aux]; apply (zero_smallest1 aux).
have pc: exists k, p k.
  exists (succ y); rewrite /p; ee.
  move: (is_lt_succ yB) => ysy.
  rewrite /g2 binom_2plus0; last by hprops.
  move: (BS_succ yB) => syB.
  have ax: (succ y) <=c (binom (succ y) 2c +c (succ y)).
    rewrite card_plusC; apply (Bsum_increasing3 syB(BS_binom syB inc2_Bnat)).
    move: (g2B _ yB)=> gB; fprops.
  co_tac.
move:(least_int_prop1 pa pb pc) => [x [xB [psx npx]]].
move: (hc _ xB) => bp.
have p1: y <=c ((g2 x) +c x).
  move: psx => [_];rewrite bp.
  rewrite (plus_via_succ _ xB).
  rewrite (lt_is_le_succ _ (BS_plus (g2B _ xB) xB)) //.
have p2: cardinal_le (g2 x) y.
  have cg2: is_cardinal (g2 x) by move: (g2B _ xB); fprops.
  have cy: is_cardinal y by fprops.
  case (cardinal_le_total_order2 cg2 cy) => h; first by exact h.
   elim npx;red; split; assumption.
move: (g2B _ xB) => g2Bx.
move: (card_sub_pr p2); set n:= (y -c (g2 x)).
move=> p3;rewrite -p3 in p1.
have nB:inc n Bnat by apply BS_sub.
move: (plus_le_simplifiable g2Bx nB xB p1) => lenx.
move: (card_sub_pr lenx); set m:= (x -c n).
move=> p4;rewrite -p4 in p3.
have mB: inc m Bnat by rewrite /m; apply BS_sub.
exists (J n m); split; first by apply product_pair_inc; exact.
by rewrite /mi pr1_pair pr2_pair card_plusC p3.
Qed.

Theorem equipotent_inf2_inf: forall a, infinite_c a ->
  a ^c 2c = a.
Proof.
move=> E ciE.
have cE:is_cardinal E by move: ciE => [ok _].
have cEE:cardinal E = E by apply cardinal_of_cardinal.
have isE:infinite_set E by red; rewrite cEE; red in ciE; intuition.
set (base := set_of_sub_functions E (product E E)).
set (pr := fun z => injection z & range (graph z) = coarse (source z)).
have [psi [psibase [prpsi ispsi]]]:
  exists psi, inc psi base & pr psi & infinite_set (source psi).
  move: (infinite_greater_countable isE) => [F [FE cFB]].
  have [f [bf [sf tf]]]: (F \Eq (product F F)).
    move:cFB; rewrite cardinal_equipotent=> eFB; eqsym.
    eqtrans (product Bnat Bnat); eqtrans Bnat.
      apply equipotent_N2_N.
    by eqsym.
  have ff: is_function f by fct_tac.
  set (y:= BL (fun z => W z f) F (product E E)).
  have pm: (sub (product F F) (product E E)) by apply product_monotone.
  have ta: (transf_axioms (fun z => W z f) F (product E E)).
     move=> t tF /=; apply pm;rewrite -tf; apply (inc_W_target ff) ;ue.
  have iy:injection y.
    apply (bl_injective ta); move: bf=> [[_ injf]_ ]; rewrite -sf; apply injf.
  exists y; split.
    rewrite /base; bw; split; [ fct_tac| rewrite /y bl_source bl_target];ee.
  split; last by rewrite /y; aw; red; rewrite cFB;apply infinite_Bnat.
  rewrite /pr; split => //;rewrite /y /BL; aw.
  have fgL: fgraph (L F (fun z : Set => W z f)) by gprops.
  set_extens t; rewrite frange_inc_rw //; bw.
    move=> [x [xF]]; bw; move=> ->; rewrite /coarse -tf.
    apply inc_W_target =>//; ue.
  move: bf=> [_ sjf]; rewrite /coarse -tf =>tt.
  move: (surjective_pr2 sjf tt) => [z []]; rewrite sf; move=> zsf <-.
  ex_tac; bw.
set (odr := opposite_order (extension_order E (product E E))).
set (ind := Zo base (fun z => pr z & sub (graph psi) (graph z))).
have oe:order (extension_order E (product E E)) by fprops.
have oo:order odr by rewrite /odr; fprops.
have so: sub ind (substrate odr) by rewrite/odr/ind; aw; apply Z_sub.
have oi: order (induced_order odr ind) by fprops.
have ii : inductive_set (induced_order odr ind).
  move=> X Xind; rewrite /total_order; aw; move => [iot tot]; awi Xind =>//.
  have Hla:forall i, inc i X -> is_function i.
    move => i iX; move: (Xind _ iX); rewrite /ind Z_rw.
    by move=> [_ [[[ok _] _] _]].
  have Hlb:forall i, inc i X -> target i = product E E.
    move => i iX; move: (Xind _ iX); rewrite /ind Z_rw/base; bw; intuition.
  have Hlc: forall x y, inc x X -> inc y X -> gle odr x y \/ gle odr y x.
    move=> x y xX yX; move: (tot _ _ xX yX);rewrite /gge; aw; apply Xind=>//.
  have Hd: forall i j, inc i X -> inc j X ->
    agrees_on (intersection2 (source i) (source j)) i j.
    move=> i j iX jX; red; ee.
        apply intersection2sub_first.
     apply intersection2sub_second.
   move=> a ;aw; move => [asi asj].
   case (Hlc _ _ iX jX)=> h; [ | symmetry ];
      apply (extension_order_pr h (x:=a)) =>//.
  have He:forall i, inc i X -> function_prop i (source i) (product E E).
    move=> i iX;red; ee.
  move: (extension_covering He Hd) => [[x [[fx [sx tx]] agx]]_].
  have xb: inc x base.
    rewrite /base; bw; ee; rewrite sx => t; srw.
    move=> [y [yX]]; move: (Xind _ yX); rewrite /ind Z_rw /base; bw; ee.
  have Hg: forall i, inc i X -> sub (graph i) (graph x).
    move=> i iX; rewrite sub_function =>//; last by apply Hla.
    move: (agx _ iX); rewrite /agrees_on; move=> [p1 [p2 p3]]; ee.
    move=> a asi; symmetry; apply p3 =>//.
  case (emptyset_dichot X)=> neX.
    exists psi; split.
      aw; rewrite /ind; apply Z_inc =>//; fprops.
    rewrite neX; move=> u ye; elim (emptyset_pr ye).
  move: neX => [y yX].
  have sgp:(sub (graph psi) (graph x)).
      apply sub_trans with (graph y); last by apply Hg.
    move: (Xind _ yX); rewrite /ind Z_rw; intuition.
  have injx: injection x.
     split=>//; move => u v;rewrite sx; srw; move=> [a [aX usa]][b [bX vsb]].
     have [z [zX [usz vsz]]]:
        (exists z, inc z X & inc u (source z) & inc v (source z)).
      move: (Hlc _ _ aX bX); rewrite /odr.
      rewrite (opposite_gle _ _ oe) (opposite_gle _ _ oe)
        ! extension_order_rw ;case; move=> [_ [_ et]];
         move: (source_extends et); [exists b | exists a ]; ee.
     move: (agx _ zX); rewrite /agrees_on; move => [_ [_ aux]].
     rewrite (aux _ usz) (aux _ vsz).
     move: (Xind _ zX); rewrite /ind Z_rw /pr; move=> [_ [[[_ iz] _] _]].
     apply iz => //.
  have rx: (range (graph x) = product (source x) (source x)).
    set_extens a; rewrite range_inc_rw//.
      move=> [b [bsx aW]]; move: bsx; rewrite sx;srw; move=> [c [cy bsc]].
      move: (agx _ cy); rewrite/agrees_on;move => [_ [_ aux]].
      rewrite (aux _ bsc) in aW.
      move: (Xind _ cy); rewrite /ind Z_rw/ pr; move=> [_ [[ic rc] _]].
      have: inc a (coarse (source c)).
        rewrite -rc aW; apply inc_W_range_graph=>//; fct_tac.
      rewrite /coarse !product_inc_rw; move=> [pa [Ps Qs]]; srw; ee; ex_tac.
    rewrite product_inc_rw sx; srw; move=> [pa [[b [bX psb]] [c [cX qsc]]]].
    have [z [zX [usz vsz]]]:
        (exists z, inc z X & inc (P a) (source z) & inc (Q a) (source z)).
      move: (Hlc _ _ bX cX).
      rewrite /odr (opposite_gle _ _ oe) (opposite_gle _ _ oe)
       ! extension_order_rw; case; move=> [_ [_ et]];
       move: (source_extends et); [exists c | exists b ]; ee.
    have :inc a (coarse (source z)) by rewrite /coarse; aw.
    move: (Xind _ zX); rewrite /ind Z_rw/ pr; move=> [_ [[ic rc] _]].
    have fz: is_function z by fct_tac.
    rewrite -rc range_inc_rw //; move=> [d [dsz]] ->.
    move: (agx _ zX); rewrite/agrees_on;move => [_ [_ aux]].
    rewrite -(aux _ dsz).
    exists d; srw; ee; ex_tac.
  have xi: (inc x ind). rewrite /ind; apply Z_inc =>//.
  exists x; split; first by aw.
  move=> z zX; move: (Xind _ zX) => zi; aw.
  move: zi; rewrite /ind Z_rw; move=> [zb _].
  rewrite /odr; aw; ee; rewrite /extends; ee.
  move: zb; rewrite /base; bw; move=>[_ [_ tz]]; rewrite tx tz; fprops.

move: (Zorn_lemma oi ii) => [x].
rewrite /maximal_element (substrate_induced_order oo so).
move=> [xi aux].
have maxp: forall u, inc u ind -> extends u x -> u = x.
   move=> u ui ue;apply aux; aw; rewrite /odr; aw.
   move: ui; rewrite /ind Z_rw; move=> [ub _].
   move: xi; rewrite /ind Z_rw; move=> [xb _].
   ee; rewrite /extends; ee.
clear aux.
move: xi; rewrite /ind Z_rw /base; bw.
move=> [[fx [ssxE txE]] [[ijx rgx] sgx]].
set (F := source x); set b:= cardinal F.
have binf:infinite_c b.
  have ss: (sub (source psi) (source x)).
    have fspi: is_function psi by move: prpsi=> [ip _]; fct_tac.
    move: (sub_graph_domain sgx); rewrite? f_domain_graph //.
  move: (sub_smaller ss); rewrite -/F -/b => p1.
  case (finite_dichot (cardinal_cardinal F)) => //.
  move=> aux; move: (le_int_is_int aux p1) => f1.
  elim (infinite_dichot2 f1 ispsi).
have bsq: (b = b *c b).
  rewrite card_mult_pr1.
  have a1: (F \Eq (coarse F)).
    rewrite /F -rgx; apply equipotent_range => //.
  rewrite /b cardinal_equipotent; eqtrans (product F F).
have cb: is_cardinal b by rewrite /b; fprops.
case (equal_or_not b E) => bE.
  by rewrite -bE power_x_2 =>//.
have bltE: (b <c E).
  split ; [move: (sub_smaller ssxE); rewrite cEE | ] => //.
have Hc: b *c 2c = b +c b by rewrite card_multC two_times_n.
have cb2b: b <=c (b *c 2c).
   by rewrite Hc; apply sum_increasing3.
have b2b2: (b *c 2c) <=c (b *c b).
  apply product_increasing2; fprops.
  have is_finite2: finite_c card_two by rewrite -inc_Bnat; fprops.
  apply (finite_le_infinite is_finite2 binf).
rewrite -bsq in b2b2.
move: (cardinal_antisymmetry1 cb2b b2b2) => b2b.
have : (b <c (cardinal(complement E F))).
  have cc: (is_cardinal (cardinal (complement E F))) by fprops.
  move: (cardinal_complement ssxE); rewrite -/F => caux.
  move: (cardinal_le_total_order2 cc cb); case; last by done.
  move => p1.
  have cbb: (b <=c b) by fprops.
  move: (sum_increasing2 cbb p1); rewrite caux -Hc -b2b cEE.
  move=> Eb; co_tac.
rewrite /cardinal_lt; move=> [lbEF _]; move: (cardinal_le_aux1 lbEF).
rewrite -(cardinal_of_cardinal cb) -eq_subset_card; move=> [Y [syc eFY]].
set (Z:= union2 F Y).
set (a1:= product F F); set (a2 := product F Y); set (a3 := product Y Z).
have dFY: disjoint F Y.
   by apply disjoint_pr; move=> u uF uy; move: (syc _ uy); srw; intuition.
have ca1: cardinal (union2 a2 a3) = b.
  have e1: F \Eq b by rewrite /b; fprops.
  have e2: Y \Eq b by eqsym.
  have e3: Z \Eq b.
    have cbb: is_cardinal (b +c b) by fprops.
    rewrite - cardinal_equipotent /Z b2b Hc (cardinal_of_cardinal cbb).
    apply card_plus_pr1 =>//.
  rewrite b2b Hc;apply card_plus_pr1.
      apply disjoint_pr; move => t; rewrite /a2 /a3; aw.
      move=> [_ [af _]][_ [ay _]]; move: (syc _ ay); srw; intuition.
    rewrite /a2 bsq card_mult_pr1; eqtrans (product b b).
  rewrite /a3 bsq card_mult_pr1; eqtrans (product b b).
have pzz: (product Z Z = union2 (product F F) (union2 a2 a3)).
  rewrite /a2 /a3 /Z; set_extens t.
    rewrite product_inc_rw !union2_rw; move=> [pt [p1 p2]].
    case p1 => r1.
      by case p2=> r2; [left | right ; left ] ;apply product_inc.
    by right; right; apply product_inc; [ | | rewrite union2_rw].
  rewrite ! union2_rw; case.
    rewrite product_inc_rw;move=> [p1 [p2 p3]].
    by apply product_inc; [| apply union2_first | apply union2_first].
  case.
     rewrite product_inc_rw;move=> [p1 [p2 p3]].
    by apply product_inc; [| apply union2_first | apply union2_second].
    rewrite product_inc_rw;move=> [p1 [p2 p3]].
    by apply product_inc; [| apply union2_second | ].
have dzz: (disjoint (product F F) (union2 a2 a3)).
  rewrite /a2 /a3 /Z; apply disjoint_pr; move=> u; aw.
  move=> [_ [pF qF]]; case.
    move=> [_ [_ qY]]; move: (syc _ qY); srw; intuition.
  move=> [_ [pY _]]; move: (syc _ pY); srw; intuition.
have: (Y \Eq (union2 a2 a3)).
   eqtrans b; first (by eqsym).
   by rewrite - cardinal_equipotent ca1; apply cardinal_of_cardinal.
move=> [x0 [bx0 [sx0 tx0]]].
set (g:= corresp Z (product E E) (union2 (graph x) (graph x0))).
have Hga: source g = Z by rewrite /g;aw.
have Hgb:graph g = (union2 (graph x) (graph x0)) by rewrite /g;aw.
have fx0: is_function x0 by fct_tac.
have Hgd: range (graph g) = coarse (source g).
  move: bx0 => [_ sjx0].
  rewrite Hga Hgb range_union2 rgx/coarse pzz -tx0 -(surjective_pr3 sjx0) //.
have Hhf: target g = product E E by rewrite /g; aw.
have Hge:domain (graph g) = (source g).
  rewrite Hgb Hga domain_union2; aw; rewrite sx0 //.
have ze: sub Z E.
  rewrite /Z; move=> t; rewrite union2_rw;case; first by rewrite/F;apply ssxE.
  move=> tY; move: (syc _ tY); srw; intuition.
have fg: is_function g.
  rewrite /g;apply is_function_pr.
      apply fgraph_union2; fprops; aw;rewrite sx0; exact dFY.
    rewrite - Hgb Hgd /coarse Hga; apply product_monotone =>//.
  by rewrite -Hgb Hge Hga.
have ig: injection g.
   have aux: forall a b c, inc (J a b) (graph x) -> inc (J c b) (graph x0) ->
    False.
     move=> u v w J1 J2.
     rewrite /disjoint in dzz; empty_tac1 v; apply intersection2_inc.
       rewrite -[product F F]/(coarse F) -rgx; dw; [ex_tac | fprops].
     rewrite -tx0; apply (inc_pr2graph_target fx0 J2).
  apply injective_pr_bis =>//; rewrite /related Hgb.
  move=> u v w; aw; case => h1; case => h2.
    apply (injective_pr3 ijx h1 h2).
    elim (aux _ _ _ h1 h2).
    elim (aux _ _ _ h2 h1).
    move: bx0 => [ijx0 _]; apply (injective_pr3 ijx0 h1 h2).
have sg: sub (graph x) (graph g) by rewrite Hgb;apply union2sub_first.
have gi: inc g ind.
  rewrite /ind /base /pr; apply Z_inc; first by bw;rewrite Hga; ee.
  ee; apply sub_trans with (graph x) =>//.
have egx: extends g x by rewrite /extends; ee; rewrite txE Hhf; fprops.
move: (maxp _ gi egx) => gz.
move: (f_equal source gz); rewrite Hga /Z => p1.
have Ye: (Y= emptyset).
   apply is_emptyset; move=> y yY; move: (syc _ yY); srw; move=> [_ yF].
   by elim yF; rewrite /F -p1; apply union2_second.
have Ye1:(cardinal Y = 0c) by rewrite Ye;apply cardinal_emptyset.
have Fe1: (b = 0c) .
  by rewrite -Ye1 -(cardinal_of_cardinal cb) cardinal_equipotent.
move: binf; rewrite Fe1 infinite_c_pr succ_zero; move=> [_ zo].
by elim card_one_not_zero.
Qed.

Lemma square_of_infinite: forall a, infinite_c a ->
   a *c a = a.
Proof.
move=> a ai.
have ca: (is_cardinal a) by move: ai => [ca _].
by rewrite -power_x_2 //; apply equipotent_inf2_inf.
Qed.

Lemma power_of_infinite: forall a n, infinite_c a -> inc n Bnat ->
  n <> 0c -> a ^c n = a.
Proof.
move=> a n ia nB nzn.
have ca: (is_cardinal a) by move: ia => [ca _].
move: (square_of_infinite ia) => aux.
move:(predc_pr nB nzn) => [qB] ->.
move: qB; set (q:= predc n). generalize q.
apply cardinal_c_induction.
  rewrite succ_zero; apply power_x_1 =>//.
by move=> m mB; rewrite (pow_succ _ (BS_succ mB)); move=> ->.
Qed.

Lemma power_of_infinite1: forall a n, infinite_c a -> inc n Bnat ->
  (a ^c n) <=c a.
Proof.
move=> a n ia nB.
have ca: (is_cardinal a) by move: ia => [ca _].
case (equal_or_not n 0c) => h.
  rewrite h power_x_0.
  have f1: finite_c card_one by rewrite -inc_Bnat; fprops.
  apply (finite_le_infinite f1 ia).
rewrite (power_of_infinite ia nB h); fprops.
Qed.

Lemma finite_family_product: forall a f, fgraph f ->
  finite_set (domain f) -> infinite_c a ->
  (forall i, inc i (domain f) -> (V i f) <=c a) ->
  (forall i, inc i (domain f) -> V i f <> 0c) ->
  (exists j, inc j (domain f) & (V j f) = a) ->
  cardinal_prod f = a.
Proof.
move=> a f fgf fsd ifa alea alnz [j0 [j0d vj0]].
set (g:= cst_graph (domain f) a).
have fgg: fgraph g by rewrite /g /cst_graph; gprops.
have df: domain f = domain g by rewrite /g/cst_graph; bw.
have le1:forall x, inc x (domain f) -> cardinal_le (V x f) (V x g).
  by move=> t tdf; rewrite /g/cst_graph; bw; apply alea.
move: (product_increasing fgf fgg df le1). rewrite/g card_pow_pr2.
set (n:= cardinal (domain f)).
have nB: (inc n Bnat) by bw.
have nz: n <> 0c by apply cardinal_nonemptyset1; exists j0 =>//.
have->: (card_pow a (domain f) = card_pow a n).
  rewrite /n;apply card_pow_pr; fprops.
rewrite (power_of_infinite ifa nB nz)=> le0.
set (j:= singleton j0).
have alc: (forall x, inc x (domain f) -> is_cardinal (V x f)).
  by move=> x xdf; move: (alea _ xdf) => [h _].
move: (alc _ j0d) => ca.
have sjd: (sub j (domain f)) by move=> t; rewrite /j singleton_rw; move=> ->.
move: (product_increasing1 fgf alc alnz sjd).
rewrite vj0 in ca.
rewrite /j trivial_cardinal_prod3 // vj0 (cardinal_of_cardinal ca).
move=> le2; co_tac.
Qed.

Lemma product2_infinite: forall a b, b <=c a ->
  infinite_c a -> b <> 0c -> a *c b = a.
Proof.
move=> a b leba ia nzb.
move :(leba) => [cb [ca _]].
have : ((a *c b) <=c (a *c a)).
  apply product_increasing2; fprops.
rewrite (square_of_infinite ia) => le1.
have le2: (a <=c (a *c b)) by apply product_increasing3.
co_tac.
Qed.

Lemma product2_infinite1: forall a b, b <=c a ->
  infinite_c a -> (a *c b) <=c a.
Proof.
move => a b leba ia.
case (equal_or_not b 0c) => h.
  rewrite h; rewrite zero_prod_absorbing.
  have f0: finite_c 0c by rewrite - inc_Bnat;fprops.
  apply (finite_le_infinite f0 ia).
move :(leba) => [_ [ca _]].
rewrite (product2_infinite leba ia h); fprops.
Qed.

Lemma product2_infinite2: forall a b, finite_c b ->
  infinite_c a -> (a *c b) <=c a.
Proof.
move => a b fb ia.
move: (finite_le_infinite fb ia) => leab.
apply (product2_infinite1 leab ia).
Qed.

Lemma notbig_family_sum: forall a f, fgraph f ->
  infinite_c a -> (cardinal (domain f)) <=c a ->
  (forall i, inc i (domain f) -> (V i f) <=c a) ->
  (cardinal_sum f) <=c a.
Proof.
move=> a f fgf ifa leda alea.
have Ha: is_cardinal a by move: ifa => [ca _].
set (g:= L (domain f) (fun _ =>a)).
have fgg: fgraph g by rewrite /g; gprops.
have dg : domain f = domain g by rewrite /g; bw.
have ale: forall x, inc x (domain f) -> cardinal_le (V x f) (V x g).
  by move=> x xdf; rewrite /g; bw; apply alea.
move: (sum_increasing fgf fgg dg ale).
rewrite sum_of_same1.
move: (product2_infinite1 leda ifa) => r1.
have ->:card_mult a (domain f) = card_mult a (cardinal (domain f)).
  symmetry;apply card_mult_pr2 => //; apply double_cardinal.
move => r2; co_tac.
Qed.

Lemma notbig_family_sum1: forall a f, fgraph f ->
  infinite_c a -> (cardinal (domain f)) <=c a ->
  (forall i, inc i (domain f) -> (V i f) <=c a) ->
  (exists j, inc j (domain f) & (V j f) = a) ->
  (cardinal_sum f) = a.
Proof.
move=> a f fgf ifa leda alea [j0 [j0d vj0]].
have ca: (is_cardinal a) by move: ifa => [ca _].
move: (notbig_family_sum fgf ifa leda alea) => le1.
have: sub (singleton j0) (domain f) by move=>t;rewrite singleton_rw; move=>->.
have: (forall x, inc x (domain f) -> is_cardinal (V x f)).
  by move=> x xdf; move: (alea _ xdf) => [ok _].
move=>p1 p2;move: (sum_increasing1 fgf p1 p2).
rewrite trivial_cardinal_sum3 // vj0 //.
rewrite (cardinal_of_cardinal ca)=> le2; co_tac.
Qed.

Lemma sum2_infinite1: forall a, infinite_c a -> a +c a = a.
Proof.
move=> a ia.
have: (card_plus a a = card_mult a card_two).
  rewrite card_multC two_times_n//.
have is_finite2: finite_c card_two by rewrite -inc_Bnat; fprops.
have le2a: cardinal_le card_two a by apply (finite_le_infinite is_finite2 ia).
have n20:card_two <> 0c by apply card_two_not_zero.
rewrite product2_infinite //; move=> <-.
Qed.

Lemma sum2_infinite: forall a b, b <=c a ->
  infinite_c a -> a +c b = a.
Proof.
move=> a b leba ia.
move :(leba) => [cb [ca _]].
have le1:(cardinal_le a (card_plus a b)) by apply sum_increasing3.
apply cardinal_antisymmetry1 =>//.
rewrite - {2} (sum2_infinite1 ia).
apply sum_increasing2; fprops.
Qed.

Lemma cardinal_comp_singl_inf: forall E x,
  infinite_set E -> cardinal E = cardinal (complement E (singleton x)).
Proof.
move=> E x iE; case (p_or_not_p (inc x E)) => xE.
  move:(cardinal_succ_pr1 E x).
  rewrite - tack_on_complement //.
  set (F:=(complement E (singleton x))) => ces.
  have cF: is_cardinal (cardinal F) by fprops.
  case (finite_dichot cF).
    rewrite (is_finite_succ cF) - ces=> h; elim (infinite_dichot2 h iE).
  by rewrite infinite_c_pr - ces; move=> [_ res].
have ->: (complement E (singleton x) = E) =>//.
set_extens t; srw; aw;[ by move=> [te _] | move=> te; ee; dneg h; ue].
Qed.

Definition countable_set E:= equipotent_to_subset E Bnat.

Lemma countable_prop: forall E,
  countable_set E = (cardinal E) <=c (cardinal Bnat).
Proof.
move=> E; rewrite - cardinal_le_aux2 /countable_set; fprops.
rewrite eq_subset_card.
apply iff_eq; [ move=> es;ee | intuition ].
Qed.

Lemma countable_finite_or_N: forall E, countable_set E ->
  finite_c (cardinal E) \/ cardinal E = cardinal Bnat.
Proof.
move=> E; rewrite countable_prop => leB.
case (finite_dichot (cardinal_cardinal E)) ; first by auto.
move=> [_ nf]; right.
move: (infinite_greater_countable1 nf) => le1; co_tac.
Qed.

Lemma countable_finite_or_N_b: forall E, countable_set E ->
  finite_set E \/ equipotent E Bnat.
Proof. move=> E cE; case (countable_finite_or_N cE); aw; auto. Qed.

Lemma countable_finite_or_N_c: forall E, countable_set E ->
  infinite_set E -> equipotent E Bnat.
Proof. move=> c cE; case (countable_finite_or_N_b cE) =>//.
move=> h1 h2; elim (infinite_dichot2 h1 h2).
Qed.

Theorem countable_subset: forall E F, sub E F -> countable_set F ->
  countable_set E.
Proof.
move=> E F EF; rewrite countable_prop countable_prop => h.
apply cardinal_le_transitive with (cardinal F) =>//; apply sub_smaller =>//.
Qed.

Theorem countable_product: forall f, fgraph f ->
  finite_set (domain f) ->
  (forall i, inc i (domain f) -> countable_set (V i f)) ->
  countable_set (productb f).
Proof.
move=> f fgf fsd alc; rewrite countable_prop.
set (g:= L(domain f) (fun i => cardinal (V i f))).
have ->:(cardinal (productb f) = cardinal_prod g).
  rewrite cardinal_prod_pr =>//.
set (h:= L(domain f)(fun i:Set => cardinal Bnat)).
apply cardinal_le_transitive with (cardinal_prod h).
  apply product_increasing.
          rewrite /g; gprops.
       rewrite /h; gprops.
    rewrite /g/h; bw.
  rewrite /g /h; bw; move=> x xdf; bw.
  by move: (alc _ xdf);rewrite countable_prop.
have ->: h = cst_graph (domain f) (cardinal Bnat) by [].
rewrite card_pow_pr2.
set (cb:= (cardinal Bnat)).
have ->: (card_pow cb (domain f) = card_pow cb (cardinal (domain f))).
  apply card_pow_pr;fprops.
move: infinite_Bnat. rewrite infinite_set_rw => aux.
apply power_of_infinite1; [apply aux | bw].
Qed.

Theorem countable_union: forall f, fgraph f ->
  countable_set (domain f) ->
  (forall i, inc i (domain f) -> countable_set (V i f)) ->
  countable_set (unionb f).
Proof.
move=> f fgf cs alc; rewrite countable_prop.
set d:= domain f.
apply cardinal_le_transitive
  with (cardinal_sum (L d (fun i => cardinal (V i f)))).
  apply cardinal_sum_pr1 =>//.
set (h:= L d (fun i:Set => cardinal Bnat)).
  apply cardinal_le_transitive with (cardinal_sum h).
  rewrite /h; apply sum_increasing; gprops; bw.
  move=> x xd; bw; move: (alc _ xd); rewrite countable_prop =>//.
rewrite sum_of_same1.
set (c := cardinal Bnat).
have ->: (card_mult c d = card_mult c (cardinal d)).
  symmetry;apply card_mult_pr2; fprops; apply double_cardinal.
apply product2_infinite1 =>//.
  move: cs; rewrite countable_prop //.
rewrite /c -infinite_set_rw; apply infinite_Bnat.
Qed.

Lemma card_bnat_not_zero: cardinal Bnat <> 0c.
Proof.
move=> bad.
move: (cardinal_nonemptyset bad) => h.
empty_tac1 0c.
Qed.

Theorem infinite_partition: forall E, infinite_set E ->
  exists f, partition_fam f E & (domain f) \Eq E &
    (forall i, inc i (domain f) -> (infinite_set (V i f) &
      countable_set (V i f))).
Proof.
move=> E iE; move: (infinite_greater_countable1 iE) => h1.
have iE': infinite_c (cardinal E) by split => //; apply cardinal_cardinal.
move: (product2_infinite h1 iE' card_bnat_not_zero).
rewrite card_mult_pr1 cardinal_equipotent; move=> [f [bf [sf tf]]].
move: (bf) => [injf sjf].
set (g:= L (cardinal E) (fun a => image_by_fun f
    (product (singleton a) (cardinal Bnat)))).
have ff: is_function f by fct_tac.
have ha: is_graph (graph f) by fprops.
have fgg: (fgraph g) by rewrite /g; gprops.
exists g; rewrite /g;ee; bw; [ | fprops | ].
  red;ee.
    apply mutually_disjoint_prop;bw; move=> i j y inE jnE; bw.
    rewrite /image_by_fun ! image_by_graph_rw; move=> [u [u1 u2]][v [v1 v2]].
    move:(injective_pr3 injf u2 v2) => uv.
   move: u1 v1;rewrite !product_inc_rw !singleton_rw.
   move=> [_ [u1 _]][_ [v1 _]]; rewrite -u1 -v1 uv //.
   set_extens t; srw; bw.
     move=> [y [ycE]].
     rewrite (L_V_rw _ ycE) /image_by_fun image_by_graph_rw -tf.
     move=> [x [xs xt]];apply (inc_pr2graph_target ff xt).
  move => tE.
  have tt: inc t (target f) by rewrite tf.
  move: (surjective_pr sjf tt);move=> [x [xsf jG]].
  move: xsf; rewrite sf product_inc_rw; move=> [pax [px qx]].
  ex_tac; rewrite (L_V_rw _ px) /image_by_fun image_by_graph_rw.
  exists x; ee; rewrite product_inc_rw singleton_rw; ee.
move => i inE; bw.
set (dom:= (product (singleton i) (cardinal Bnat))).
have sd: (sub dom (source f)). rewrite sf/dom; move=> t; aw.
  move=> [pt [pti qt]]; rewrite pti; ee.
have aux: (cardinal (image_by_fun f dom) = cardinal Bnat).
  aw; eqtrans dom.
    eqsym;apply (equipotent_restriction1 sd injf).
  rewrite /dom; eqtrans (cardinal Bnat).
  eqtrans (product (cardinal Bnat) (singleton i)).
  apply equipotent_product_sym.
  eqsym; apply equipotent_prod_singleton.
split.
  red; rewrite aux; apply infinite_Bnat.
by rewrite countable_prop; rewrite aux; fprops.
Qed.

Lemma countable_inv_image: forall f, surjection f ->
  (forall y, inc y (target f) ->
    countable_set (inv_image_by_fun f (singleton y))) ->
  infinite_set (target f) ->
  (source f) \Eq (target f).
Proof.
move => f sf alc it.
have ff: is_function f by fct_tac.
set (pa := L (target f) (fun z=> (inv_image_by_fun f (singleton z)))).
have upa: (unionb pa = (source f)).
  rewrite /pa; set_extens t; srw; rewrite /inv_image_by_fun;bw.
    move=> [y [tf]]; bw; aw; move=> [u []]; aw; move=> -> Jg; graph_tac.
  move => tf; exists (W t f).
  move: (inc_W_target ff tf) => wt; ee; bw; aw; ex_tac; apply W_pr3 =>//.
have md: (mutually_disjoint pa).
  rewrite /pa;apply mutually_disjoint_prop;bw.
  move=> i j y itf jtf; bw; rewrite /inv_image_by_fun; aw.
  move=> [u [ui Jg1]] [v [vi Jg2]].
  by move: ui vi; aw; move=> <- <-; rewrite- (W_pr ff Jg1) - (W_pr ff Jg2).
have fgp: fgraph pa by rewrite /pa; gprops.
move: (cardinal_sum_pr fgp).
rewrite /disjoint_union.
have: (equipotent (unionb (disjoint_union_fam pa)) (unionb pa)).
  apply equipotent_disjoint_union => //.
        rewrite /pa /disjoint_union_fam; gprops.
      rewrite/disjoint_union_fam /pa; bw.
    rewrite /disjoint_union_fam /pa; bw; move=> i idf; bw.
    eqsym; apply equipotent_prod_singleton.
  apply disjoint_union_disjoint => //.
rewrite - cardinal_equipotent; move => ->; rewrite upa.
rewrite - cardinal_equipotent.
set (cf:= L (domain pa) (fun a : Set => cardinal (V a pa))).
move => aux.
set (g:= L (domain pa) (fun _:Set => cardinal Bnat)).
have : (cardinal_le (cardinal (source f)) (cardinal_sum g)).
  rewrite aux /cf /g /pa;apply sum_increasing; [gprops | gprops | bw |].
  bw; move => x xa; bw; rewrite - countable_prop; apply alc =>//.
rewrite sum_of_same1.
have ->:(card_mult (cardinal Bnat) (domain pa) = cardinal (target f)).
  rewrite /pa; bw;
  transitivity (card_mult (cardinal Bnat) (cardinal (target f))).
    apply card_mult_pr2; [ trivial | by rewrite double_cardinal].
  set (u:= cardinal (target f)).
  rewrite card_multC; apply product2_infinite.
      apply infinite_greater_countable1 =>//.
    split; first (by apply cardinal_cardinal); done.
  apply card_bnat_not_zero.
move => le1.
have le2: (cardinal_le (cardinal (target f)) (cardinal (source f))).
  apply surjective_cardinal_le; exists f; ee.
co_tac.
Qed.

Theorem infinite_finite_subsets: forall E, infinite_set E ->
  (Zo (powerset E) (fun z => finite_set z)) \Eq E.
Proof.
move=> E inE.
have icE: infinite_c (cardinal E) by split; [apply cardinal_cardinal | exact].
set bF:=Zo _ _ .
set (T:=fun n => Zo (powerset E) (fun z => cardinal z = n)).
have le1: (forall n, inc n Bnat -> cardinal_le (cardinal (T n)) (cardinal E)).
  move=> n nB; rewrite /T.
  have cn: (cardinal n = n) by rewrite cardinal_of_cardinal; fprops.
  set (K:= Zo(set_of_functions n E)(fun z => injection z)).
  set (f:= BL (fun z => range (graph z)) K (T n)).
  have ta: transf_axioms (fun z => range (graph z)) K (T n).
    move=> z; rewrite /K /T Z_rw Z_rw; aw;move=> [[fz [sz tz]] inz].
    rewrite -tz; ee. apply f_range_graph => //.
    by symmetry;rewrite - cn -sz; aw; apply equipotent_range.
  have ff: is_function f by rewrite /f; apply bl_function => //.
  set (q:= set_of_permutations n).
  set (c := cardinal q).
  have fc: (finite_c c).
    rewrite /c /q.
    have fsn: finite_set n by rewrite /finite_set cn - inc_Bnat.
    rewrite (number_of_permutations fsn) - inc_Bnat.
    by apply BS_factorial; ue.
  have cii: (forall x, inc x (target f) ->
    cardinal (inv_image_by_fun f (singleton x)) = c).
     move=> x ; rewrite/f /c /T; aw; rewrite Z_rw; move => [xE cx].
    have : (equipotent n x) by rewrite - cx; fprops.
    move=> [x0 [bx0 [sx0 tx0]]].
    set (x1:= corresp n E (graph x0)).
    have sx1: (source x1 = n) by rewrite /x1; aw.
    have tx1: (target x1 = E) by rewrite /x1; aw.
    have ix1: (injection x1).
      have fx0: is_function x0 by fct_tac.
      apply injective_pr_bis.
         rewrite /x1; apply is_function_pr.
             fprops.
           apply sub_trans with (target x0).
             apply f_range_graph => //.
           rewrite tx0; move: xE; aw.
         aw; ue.
      rewrite /x1; aw;move=> u v w p1 p2; move: bx0 => [injx0 _].
      apply (injective_pr injx0 p1 p2).
    set iif := inv_image_by_fun _ _.
    set (g:= BL (fun z=> (compose x1 z)) q iif).
    have ta2: (transf_axioms (fun z=> (compose x1 z)) q iif).
      rewrite/q/iif; move=> z zq; rewrite /inv_image_by_fun;aw.
      ex_tac.
      move: zq; rewrite /set_of_permutations Z_rw; aw.
      move=> [[fz [sz tz]] bz].
      have cxz: (composable x1 z) by red; ee; [ fct_tac | ue].
      set (t:= compose x1 z).
      have fr: (is_function t) by rewrite /t; fct_tac.
      have tk: (inc t K).
        rewrite /K Z_rw; aw; ee; try (solve [rewrite /t; aw]).
        apply inj_compose1 =>//; [ move: bz => [iz _] => // | ue].
      have gz: is_graph (graph z) by fprops.
      have ->: (x = W t f).
        rewrite /f/t/compose; aw; rewrite compose_range //.
         have ->: (range (graph z) = n).
           move: bz => [_ bz]; rewrite (surjective_pr3 bz)=> //.
        rewrite /x1; aw; move: bx0 => [_]; rewrite /surjection/image_of_fun.
        rewrite sx0 tx0; move=> [_ h]; rewrite -h //.
      apply W_pr3 => //.
    aw.
    have fg: is_function g by rewrite /g; apply bl_function =>//.
    eqsym; exists g; ee; rewrite /g; aw.
    apply bl_bijective => //.
        rewrite /q;move=> u v; rewrite /set_of_permutations Z_rw Z_rw.
        aw; move=> [[fu [su tu]] bu][[fv [sv tv]] bv] sc.
        apply function_exten; try fct_tac; try ue.
        move=> w wsu.
        have : (W w (compose x1 u) = W w (compose x1 v)) by ue.
        have c1: composable x1 v by red; ee; try fct_tac; try ue.
        have c2: composable x1 u by red; ee; try fct_tac; try ue.
        have wsv :inc w (source v) by rewrite sv -su.
        aw; move: ix1 => [fx1 ix1]; apply ix1.
          rewrite sx1 -tu; apply inc_W_target=> //;fct_tac.
          rewrite sx1 -tv; apply inc_W_target=> //;fct_tac.
     move => y.
     rewrite /iif /q /inv_image_by_fun; aw; move=>[u []]; aw.
     move=> -> Jg.
     move:(inc_pr1graph_source ff Jg) => ysf.
     move: ysf; rewrite /f; aw => yK.
     move: (W_pr ff Jg); rewrite /f bl_W => // rg1.
     have ww: sub (range (graph y)) (range (graph x1)).
       rewrite rg1 /x1; aw.
       move: bx0 => [_ bx0]; rewrite (surjective_pr3 bx0) tx0; fprops.
     move: yK; rewrite /K Z_rw; aw; move=> [[fy [sy ty]] iy].
     rewrite -tx1 in ty; rewrite -(exists_right_composable fy ix1 ty) in ww.
     move: ww => [h [cph ch]]; exists h; ee.
     have sh: (source h = n) by rewrite -sy - ch; aw.
     have th: (target h = n) by move: cph => [_ [_ hq]]; rewrite -hq.
     have ih: injection h.
       split;first by fct_tac.
       move => v w vsh wsh sw.
       have: W v y = W w y by rewrite - ch; aw; rewrite sw.
       move:iy => [_ aux]; apply aux; [rewrite sy -sh // |rewrite sy -sh //].
    have bh: bijection h.
      apply bijective_if_same_finite_c_inj => //.
          rewrite sh th //.
        by rewrite sh/ finite_set cn -inc_Bnat.
    rewrite /set_of_permutations; apply Z_inc; aw; ee; fct_tac.
  move: (shepherd_principle ff cii).
  rewrite /f; aw; move => cK.
  case (equal_or_not n 0c) => nz.
    rewrite nz.
    have ->: (cardinal (T 0c) = card_one).
      have ->: (T 0c = singleton emptyset).
        rewrite /T;set_extens u; aw; rewrite Z_rw.
          move=> [_ aux]; rewrite (cardinal_nonemptyset aux) //.
        move => ->; aw; split; [ apply emptyset_sub_any | apply cardinal_emptyset].
      apply cardinal_singleton.
    apply finite_le_infinite; [by rewrite - inc_Bnat; fprops | exact].
  case (finite_dichot (cardinal_cardinal (T n))) => finT.
    apply finite_le_infinite =>//.
  change (cardinal_le (cardinal (T n)) (cardinal E)).
  set (K1:= cardinal (set_of_functions n E)).
  have k1E: (K1 = cardinal E).
    rewrite /K1; change (card_pow E n = cardinal E).
    have ->: (card_pow E n = card_pow (cardinal E) n)
      by apply card_pow_pr;fprops.
    apply power_of_infinite => //.
  have le1: (cardinal_le (cardinal K) (cardinal E)).
     rewrite -k1E /K1; apply sub_smaller; rewrite /K; apply Z_sub.
  apply cardinal_le_transitive with (cardinal K) => //.
  rewrite cK.
  have i2: (cardinal_le c (cardinal (T n))) by apply finite_le_infinite.
  have i3: (c <> 0c).
    rewrite /c/q.
    have fsn: finite_set n by rewrite /finite_set cn - inc_Bnat.
     rewrite (number_of_permutations fsn).
     rewrite cn; apply (factorial_nonzero nB).
  rewrite (product2_infinite i2 finT i3); fprops.
set (Fn := L Bnat (fun n => Zo (powerset E) (fun z => cardinal z = n))).
have bfu: (bF = unionb Fn).
  rewrite /bF /Fn; set_extens t; srw; bw; rewrite Z_rw.
    move=> [tp fst]; exists (cardinal t).
    red in fst; have a1: inc (cardinal t) Bnat by bw.
    ee; bw; apply Z_inc =>//.
  move=> [y [yB]]; bw; rewrite Z_rw /finite_set - inc_Bnat.
  move=> [tE] ->; ee.
  have euu: (equipotent (unionb (disjoint_union_fam Fn)) (unionb Fn)).
       apply equipotent_disjoint_union.
                rewrite /Fn/disjoint_union_fam; gprops.
              rewrite /Fn; gprops.
            rewrite /disjoint_union_fam; bw.
          rewrite /disjoint_union_fam; bw; move=> i id.
          bw; eqsym; apply equipotent_prod_singleton.
        apply disjoint_union_disjoint; rewrite /Fn; gprops.
      apply mutually_disjoint_prop; rewrite /Fn; bw.
      move=> i j y iB jB; bw; rewrite Z_rw Z_rw; move=> [_ a1][_ a2].
      rewrite -a1 -a2 //.
rewrite - cardinal_equipotent -bfu in euu.
have fgFn: (fgraph Fn) by rewrite /Fn; gprops.
move: (cardinal_sum_pr fgFn).
rewrite /disjoint_union euu => cbf.
have: (cardinal_le
       (cardinal_sum (L (domain Fn)(fun a => cardinal (V a Fn))))
    (cardinal_sum (L (domain Fn) (fun a : Set => cardinal E)))).
  apply sum_increasing; gprops; bw; rewrite /Fn;bw; move=> x xd; bw.
  change (cardinal_le (cardinal (T x)) (cardinal E)).
  apply le1 =>//.
rewrite sum_of_same1 - cbf.
have ->: (card_mult (cardinal E) (domain Fn) = cardinal E).
  rewrite /Fn; bw.
  have ->:card_mult (cardinal E)Bnat = card_mult (cardinal E) (cardinal Bnat).
    apply card_mult_pr2;[ exact | by rewrite double_cardinal].
  apply product2_infinite.
      apply infinite_greater_countable1 =>//.
    exact.
  apply card_bnat_not_zero.
have : (cardinal_le (cardinal E) (cardinal bF)).
  rewrite - eq_subset_card1 eq_subset_ex_inj.
  exists (BL (fun x => singleton x) E bF); ee; aw.
  apply bl_injective.
    move=> x xe /=; rewrite/bF; apply Z_inc; aw.
      move=> u; aw;move=> -> //.
    red; rewrite cardinal_singleton; rewrite -inc_Bnat; fprops.
  move=> u v uE vE;apply singleton_inj.
move=> lea leb.
rewrite - cardinal_equipotent; co_tac.
Qed.

Lemma infinite_finite_sequence: forall E, infinite_set E ->
 (Zo(set_of_sub_functions Bnat E) (fun z=> finite_set (source z))) \Eq E.
Proof.
move=> E iE.
have iE': infinite_c (cardinal E) by rewrite -infinite_set_rw.
set q:= Zo _ _.
rewrite - cardinal_equipotent; apply cardinal_antisymmetry1.
  move: (infinite_finite_subsets infinite_Bnat).
  set Fn:=Zo _ _; move=> fse.
  have qu:q = unionb (L Fn (fun z=> (set_of_functions z E))).
    rewrite /q/Fn; set_extens t; rewrite Z_rw;srw; bw.
      set z := Zo _ _; move=> [[ft [sst tt]] fst].
      have aux: (inc (source t) z) by rewrite /z; apply Z_inc; aw.
      ex_tac; bw; aw; ee.
    move => [y [yz]];bw; move: yz; aw; rewrite Z_rw; aw.
    move=>[yB fsy][ft [st tt]]; rewrite st;ee.
  have ze: (forall z, inc z Fn -> cardinal_le
    (cardinal (set_of_functions z E)) (cardinal E)).
    move=> z zFn; change (cardinal_le (card_pow E z) (cardinal E)).
    have ->: (card_pow E z = card_pow (cardinal E) (cardinal z)).
    apply card_pow_pr; fprops.
    apply power_of_infinite1 =>//.
    by move: zFn; rewrite /Fn Z_rw inc_Bnat/finite_set; move=> [_].
  have fg:(fgraph (L Fn (fun z : Set => set_of_functions z E))) by gprops.
  move: (cardinal_sum_pr1 fg); rewrite -qu; bw.
  set (g:= (L Fn (fun _:Set => cardinal E))).
  set f0:= (L Fn _ ).
  have fg1: (fgraph f0) by rewrite /f0; gprops.
  have fg2: (fgraph g) by rewrite /g; gprops.
  have df0g: domain f0 = domain g by rewrite /f0 /g; bw.
  have ale: (forall x, inc x (domain f0) -> cardinal_le (V x f0) (V x g)).
    by rewrite /f0/g; bw;move=> x xdf; bw; apply ze.
  move: (sum_increasing fg1 fg2 df0g ale) => le1 le2.
  move: (infinite_greater_countable1 iE) => le3.
  move: (product2_infinite1 le3 iE').
  have <-: (cardinal Fn = cardinal Bnat) by aw.
  have ->: (card_mult (cardinal E) (cardinal Fn) = card_mult (cardinal E) Fn).
    apply card_mult_pr2; fprops; apply double_cardinal.
  rewrite sum_of_same1 in le1.
  move: (cardinal_le_transitive le2 le1) => le4 le5; co_tac.
rewrite -eq_subset_card1 eq_subset_ex_inj.
have aux: forall v, inc v E ->
   transf_axioms (fun _ => v) (singleton 0c) E by move=> vE t //=.
exists (BL (fun z => (BL ((fun _:Set => z))(singleton 0c) E)) E q).
ee;aw; apply bl_injective.
  move=> z zE; rewrite /q; apply Z_inc.
    bw; aw; ee; last by apply sub_singleton; fprops.
    apply bl_function =>//.
  aw;red;rewrite cardinal_singleton -inc_Bnat; fprops.
move=> u v uE vE sv.
have zs: (inc 0c (singleton 0c)) by fprops.
move: (f_equal (W 0c) sv); aw; apply aux =>//.
Qed.