Library ssete5

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset13 sset15 ssete4.

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

Module Exercise5.

Lemma Exercise5_1 p n q :
   inc n Bnat -> p <=c n -> q <c p ->
   binom n p = card_sumb (interval_cc Bnat_order q (n -c p +c q)) (fun k =>
    binom (n-c (succ k)) (p -c (succ q)) *c binom k q).
Proof.
move => nB lepn ltpq.
move: (BS_le_int lepn nB) => pB.
move: (BS_le_int (proj1 ltpq) pB) => qB.
set E := (Bint n).
set bigset := subsets_with_p_elements p E.
have ce: cardinal E = n by rewrite (card_Bint nB).
pose EV X := select (fun x => cardinal (X \cap (Bint x)) = q) X.
have PA: cardinal bigset = binom n p.
  by rewrite (subsets_with_p_elements_pr nB pB ce).
have PB: forall X, inc X bigset ->
  exists ! x, inc x X /\ cardinal (X \cap (Bint x)) = q.
  move => X /Zo_P [] /setP_P XE cx.
  pose f x := cardinal (X \cap Bint x).
  have f0: f \0c = \0c.
     have aux:(X \cap emptyset) = emptyset.
       by apply /set0_P => t /setI2_P [_] /in_set0.
     by rewrite /f Bint_co00 aux cardinal_set0.
  have fn: f n = p by rewrite /f -/E; move /setI2id_Pl: XE => ->.
  have pa: forall x, inc x Bnat ->
      Bint x +s1 x = Bint (succ x).
    move => x xn; exact (proj1 (Bint_pr4 xn)).
  have pb: forall x, inc x Bnat -> X \cap Bint (succ x) =
     (X \cap Bint x) \cup (X \cap singleton x).
    by move => x xb; rewrite - set_IU2r - (pa _ xb).
  have fnok: forall x, inc x Bnat -> ~(inc x X) -> f x = f (succ x).
    move => x xB xX; rewrite /f - (pa _ xB); congr (cardinal _).
    set_extens t; move => /setI2_P [sa sb]; apply /setI2_P; split;fprops.
    by case /setU1_P: sb => // xt; case: xX; rewrite - xt.
  have fok: forall x, inc x Bnat -> (inc x X) -> succ (f x) = f (succ x).
    move => x xB xX; rewrite /f (pb _ xB).
    have ->: (X \cap singleton x) = singleton x.
       apply: set1_pr; fprops.
       by move => z /setI2_P [_] /set1_P.
    by rewrite card_succ_pr //; move /setI2_P => [_] /(BintP xB) [].
  have cax: forall x, cardinalp (f x) by rewrite /f; fprops.
  have fm: forall x y, inc x Bnat -> inc y Bnat -> f x <=c f (x +c y).
     move => x y xb yb; move: y yb x xb; apply: cardinal_c_induction.
       move => x xb; aw; fprops.
     move => m mB hrec x xb; move: (hrec _ xb) => pc; apply: (card_leT pc).
     rewrite (csum_via_succ _ mB); case: (inc_or_not (x +c m) X) => h.
       rewrite - (fok _ (BS_sum xb mB) h); apply:card_le_succ0; fprops.
       rewrite - (fnok _ (BS_sum xb mB) h); fprops.
  have fxb: forall x, inc (f x) Bnat.
     move => x; rewrite /f.
     have h: sub (X \cap Bint x) X by apply: subsetI2l.
     move: (sub_smaller h); rewrite cx => ha.
     by move:(BS_le_int ha pB).
  have fm1: forall x y, inc x Bnat -> inc y Bnat -> x <c y -> inc x X ->
       f x <c f y.
    move => x y xb yb xy xx; move: (fok _ xb xx) => pc.
    apply /(card_le_succ_ltP _ (fxb x)).
    have ha: succ x <=c y by apply / (card_le_succ_ltP _ xb).
    rewrite - (cdiff_pr ha) pc; apply: fm; fprops.
  have XB: sub X Bnat by move => t tx; exact: (Bint_S1 (XE _ tx)).
  apply /unique_existence;split; last first.
    move => x y [xx xv][yx yv] ;move: (XB _ xx) (XB _ yx) => xb yb.
    case: (card_le_to_ell (CS_Bnat xb)(CS_Bnat yb)) => // ha.
      by move: (fm1 _ _ xb yb ha xx) => [_]; rewrite /f xv yv.
      by move: (fm1 _ _ yb xb ha yx) => [_]; rewrite /f xv yv.
  pose pr x := inc x Bnat /\ q <c f x.
  have pc: (forall x, pr x -> inc x Bnat) by move => x [].
  have pd: exists x, pr x by exists n; split => //; rewrite fn.
  move: (least_int_prop pc pd); case.
    rewrite /pr f0;move => [_ pe]; case: (card_lt0 pe).
  move => [x [xn [pe pf pg]]].
  exists x; case: (inc_or_not x X) => xx; last first.
    by case: pg; split => //;rewrite (fnok _ xn xx).
  move: pf; rewrite - (fok _ xn xx); move /(card_lt_succ_leP (fxb x)) => ph.
  split => //; ex_middle eq1; case: pg;split => //; split => //; fprops.
have PC: forall X, inc X bigset ->
  ( cardinal (X \cap (Bint (EV X))) = q /\ inc (EV X) X).
  move => X xb; move:(PB _ xb) => [z [[za zb] zc]]; apply: select_pr.
      ex_tac.
  by move => a b p1 p2 p3 p4; rewrite - (zc _ (conj p1 p2)) (zc _ (conj p3 p4)).
have PD: forall X, inc X bigset ->
  inc (EV X) (interval_cc Bnat_order q (n -c p +c q)).
  move => X px;move: (PC _ px) => [pc pd].
  move: px => /Zo_P [] /setP_P pa pb.
  have sc: inc ((n -c p) +c q) Bnat by fprops.
  move: (Bint_S1 (pa _ pd)) => xB.
  set int := (Bint (EV X)).
  move: (sub_smaller (@subsetI2r X int)); rewrite pc (card_Bint xB) => pe.
  apply /(Bint_ccP1 qB sc); split => //.
  have pf: sub (X \cap int) (X \cap E).
    by move => T /setI2_P [tx ti]; apply /setI2_P;split => //; apply: pa.
  have pg: cardinal (X \cap E) = p by move /setI2id_Pl: pa => ->.
  have ph: finite_set (X\cap E) by red; rewrite pg; apply /BnatP.
  move: (pa _ pd) => /(BintP nB) [ltxn _].
  have pf': sub int E by apply (Bint_M1) => //.
  have pg': cardinal E = n by rewrite (card_Bint nB).
  have ph': finite_set E by red; rewrite pg'; apply /BnatP.
  move: (cardinal_setC4 pf' ph'); rewrite pg' (card_Bint xB).
  move: (cardinal_setC4 pf ph); rewrite pg pc.
  have <-: X \cap (E -s int) = X \cap E -s (X \cap int).
     set_extens t.
       move =>/setI2_P [tx] /setC_P [t1 t2];apply /setC_P; split => //.
       apply /setI2_P => //.
       by move /setI2_P => [].
    move /setC_P => [] /setI2_P [t1 t2] t3; apply /setI2_P; split => //.
    by apply /setC_P;split => // ti; case: t3; apply /setI2_P.
  move => sa sb;move: (sub_smaller (@subsetI2r X (E -s int))).
  rewrite sa sb.
  move: (cdiff_pr (proj1 ltpq)); set pq := (p -c q) => sd.
  have pqB: inc pq Bnat by rewrite /pq; fprops.
  have ->: (n -c p) +c q = n -c pq.
      move: (cdiff_pr lepn); set np := (n -c p); rewrite - sd.
    rewrite csumC csumA; move => <-; symmetry; apply:cdiff_pr1; fprops.
  move: (cdiff_pr ltxn); set nx := n -c (EV X); move => <- => h.
  move: (cdiff_pr h); set y := (nx -c pq) => <-.
  have yB:inc y Bnat by apply : (BS_diff); apply : (BS_diff).
  rewrite (csumC pq) (csumA) (cdiff_pr1 (BS_sum xB yB) pqB).
  by exact: (csum_M0le y (CS_Bnat xB)).
transitivity (card_sumb (interval_cc Bnat_order q (n -c p +c q)) (fun k =>
     cardinal ( Zo bigset (fun X => EV X = k)))).
  rewrite -PA; apply:card_partition_induced; apply:PD.
rewrite /card_sumb; apply: f_equal.
apply: Lg_exten => k /Bint_ccP [_ [_ _ lin]].
have ly1: (n -c p +c q) <c n.
  move: (cdiff_pr lepn); set np := (n -c p) => <-.
  rewrite csumC; exact (csum_Mlteq (BS_diff _ nB) pB ltpq).
have ltkn: k <c n by co_tac.
move: (BS_le_int (proj1 ltkn) nB) => kB.
move: (BS_succ kB) => sk.
move/ (card_le_succ_ltP _ kB): (ltkn) => leskn.
move /(card_le_succ_ltP _ qB): (ltpq) => lesqp.
move: (cdiff_pr lesqp); set q':= (p -c succ q) => eq1.
set I2 := E -s (Bintc k).
have i2p:I2 = E -s Bint (succ k) by rewrite - (Bint_co_cc kB).
have ci2: cardinal I2 = (n -c succ k).
  have pf': sub (Bint (succ k)) E by apply (Bint_M1).
  have pg': cardinal E = n by rewrite (card_Bint nB).
  have ph': finite_set E by red; rewrite pg'; apply /BnatP.
  by move: (cardinal_setC4 pf' ph'); rewrite pg' i2p (card_Bint sk).
have q'B: inc q' Bnat by rewrite /q'; fprops.
have nskB: inc (n -c succ k) Bnat by fprops.
move: (subsets_with_p_elements_pr kB qB (card_Bint kB)).
move: (subsets_with_p_elements_pr nskB q'B ci2).
set Y:= subsets_with_p_elements _ _.
set Z := subsets_with_p_elements _ _ => -> ->.
have ->: cardinal Y *c cardinal Z = cardinal (Y \times Z).
  rewrite - cprod2_pr1;apply cprod2_pr2; apply: double_cardinal.
symmetry;apply /card_eqP.
pose f z := (P z \cup Q z) +s1 k.
exists (Lf f (Y \times Z) (Zo bigset (fun X => EV X = k))).
have ci2b: inc (cardinal I2) Bnat by rewrite ci2; fprops.
have la:lf_axiom f (Y \times Z) (Zo bigset (fun X => EV X = k)).
  move => u /setX_P [pu ] /Zo_P [] /setP_P pa pb /Zo_P [] /setP_P pc pd.
  have pe: sub ((P u \cup Q u) +s1 k) E.
    move => t; case /setU1_P.
       case /setU2_P => ta; first by move /setC_P: (pa _ ta) => [].
       move: (pc _ ta) => /(BintP kB) tk; apply /(BintP nB); co_tac.
    by move => ->; apply /(BintP nB).
  have pf: cardinal ((P u \cup Q u) +s1 k) = p.
    have nku: ~ inc k (P u \cup Q u).
      move /setU2_P; case => h.
        move: (pa _ h); rewrite i2p; move=> /setC_P [_]; case.
            apply/(BintsP kB); fprops.
      by move: (pc _ h) => /(BintP kB) [_].
    rewrite (card_succ_pr nku).
    have di: disjoint (P u) (Q u).
        apply disjoint_pr => t ta tb.
         move: (pa _ ta); rewrite i2p; move=> /setC_P [_]; case.
       by move: (pc _ tb) =>/ (BintP kB) [le1 _]; apply /(BintsP kB).
    rewrite (csum2_pr5 di) - csum2_pr2b - csum2_pr2a pb pd.
    rewrite - (csum_via_succ _ qB) cdiff_rpr //.
  have pg: inc (f u) bigset by apply /Zo_P; split => //; apply /setP_P.
  apply /Zo_P; split; first by exact.
  have ph:inc k (f u) /\ cardinal (f u \cap Bint k) = q.
    split; first by apply /setU1_P; right.
    suff: ((P u \cup Q u) +s1 k) \cap Bint k = Q u.
       by rewrite /f => ->.
    set_extens t; last by move => ts; apply /setI2_P; split;fprops.
    move /setI2_P => [sa] /(BintP kB) [tk1 tk2]; case /setU1_P: sa =>//.
     case /setU2_P => // tp; move: (pa _ tp).
     by rewrite i2p => /setC_P [te] /(BintsP kB).
  set s := EV (f u).
  have pi:inc s (f u) /\ cardinal (f u \cap Bint s) = q.
    by move: (PC _ pg)=> [sa sb].
  move/unique_existence: (PB _ pg) => [_ h]; exact (h _ _ pi ph).
have fi: forall u v,
  inc u (Y \times Z) -> inc v (Y \times Z) -> f u = f v -> u = v.
  have aux: forall u, inc u (Y \times Z) ->
    u = J (f u \cap I2) (f u \cap (Bint k)).
     move => u /setX_P [pu ] /Zo_P [] /setP_P pa _ /Zo_P [] /setP_P pb _.
     rewrite - {1} pu /f; congr (J _ _).
     set_extens t.
         move => ts; apply /setI2_P; split;fprops.
       move /setI2_P => [sa]; rewrite i2p => /setC_P [te] /(BintsP kB).
       move => tk;case /setU1_P: sa.
       by case /setU2_P => // tq; move /(BintP kB): (pb _ tq) => [tk1 _].
       move => tk1; case: tk; rewrite tk1; fprops.
    set_extens t.
        move => ts; apply /setI2_P; split;fprops.
      move /setI2_P => [sa] /(BintP kB) [tk1 tk2]; case /setU1_P: sa =>//.
      case /setU2_P => // tp; move: (pa _ tp).
      by rewrite i2p => /setC_P [te] /(BintsP kB).
  move => u v pu pv sv.
  by rewrite (aux _ pu) (aux _ pv) sv.
split; aw; apply: lf_bijective => //.
move => y /Zo_P [pa pb].
move: (PC _ pa); rewrite pb; move => [pc pd].
set A:=(y \cap Bint k); set B:= (y -s A) -s1 k.
have ay: sub A y by apply subsetI2l.
have Az: inc A Z by apply /Zo_P;split => //; apply /setP_P; apply: subsetI2r.
move: pa => /Zo_P []/setP_P y1 y2.
have b2: sub B I2.
  rewrite i2p;move => t /setC1_P [] /setC_P [ta tb] tc; apply /setC_P.
  split;fprops; move /(BintsP kB) => tk; case: tb; apply /setI2_P.
    split => //;by apply /(BintP kB); split.
  have pa: inc k (y -s A).
     by apply /setC_P;split => //; move /setI2_P => [_] /(BintP kB) [].
  move: (cardinal_setC2 ay);rewrite y2 - csum2_pr2a pc - csum2_pr2b.
  rewrite(card_succ_pr2 pa) -/B - eq1.
  move: (BS_le_int(sub_smaller b2) ci2b) => cbb.
  rewrite (csum_via_succ _ cbb) - (csum_via_succ1 _ qB) => h.
  move: (csum_simplifiable_left (BS_succ qB) q'B cbb h) => h1.
  have By: inc B Y by apply /Zo_P;split => //; apply /setP_P.
  exists (J B A); first by apply:setXp_i.
  rewrite /f; aw; set_extens t; last first.
    case /setU1_P; last by move => -> ;apply: pd.
    by case /setU2_P; [ move => /setC1_P [] /setC_P [] | move /setI2_P=> []].
  move => ty; apply /setU1_P;case: (equal_or_not t k) => tk //; first by right.
  left; apply /setU2_P; case: (inc_or_not t A) => ta; first by right.
  by left; apply /setC1_P;split => //; apply /setC_P.
Qed.

Lemma Exercise5_2 E
  (fs_even := Zo (powerset E) (fun z => even_int (cardinal z)))
  (fs_odd := Zo (powerset E) (fun z => odd_int (cardinal z))):
  finite_set E -> nonempty E -> fs_even \Eq fs_odd.
Proof.
move => fse nne.
set n := cardinal E.
pose ce := complement E.
have cs1: forall X, sub (ce X) E by move => X; apply: sub_setC.
have ce2: forall X, sub X E -> cardinal X +c cardinal (ce X) = n.
   by move => x xe; rewrite csum2_pr2b csum2_pr2a - cardinal_setC2.
have fsx: forall X, sub X E -> inc (cardinal X) Bnat.
   move => x xe; apply /BnatP; apply: (sub_finite_set xe fse).
have cs3: forall X, inc (cardinal (ce X)) Bnat by move => X; apply: fsx.
have cs4: forall X, sub X E -> ce (ce X) = X.
   by move => X; apply:setC_K.
have nB: inc n Bnat by move: fse => /BnatP.
case: (equal_or_not (card_rem n \2c) \0c) => nev; last first.
  have oddn: odd_int n by split => //; move => [ta tb].
  exists (Lf ce fs_even fs_odd);split; aw; apply: lf_bijective.
      move => c /Zo_P [] /setP_P cee evc; apply /Zo_P;split => //.
        by apply /setP_P.
      split; [by apply: cs3 | move => cxe].
      move: (even_odd_sum (cardinal c) (cardinal (ce c))) => [_ _ eee].
      by move: (eee evc cxe); rewrite (ce2 _ cee); move =>[].
    move => u v /Zo_P [] /setP_P uE _ /Zo_P [] /setP_P vE _ eq.
    by move: (f_equal ce eq); rewrite (cs4 _ uE) (cs4 _ vE).
  move => y => /Zo_P [] /setP_P ye yo.
  move: (cs1 y) => xe; rewrite - (cs4 _ ye); exists (ce y)=> //.
  apply: Zo_i; [by apply /setP_P | ex_middle ceo1].
  have ceo: odd_int (cardinal (ce y)) by [].
  move: (even_odd_sum (cardinal y) (cardinal (ce y))) => [eee _].
  by move: (eee yo ceo); rewrite (ce2 _ ye);move =>[].
have ece: even_int n by split.
have ce_e: forall X, sub X E -> even_int (cardinal X) ->
    even_int (cardinal (ce X)).
  move=> X XE ecx; ex_middle ceo1.
  have ceo: odd_int (cardinal (ce X)) by [].
  move: (even_odd_sum (cardinal X) (cardinal (ce X))) => [_ ee _].
   by move: (ee ecx ceo);rewrite (ce2 _ XE); move => [].
have ce_o: forall X, sub X E -> odd_int (cardinal X) ->
    odd_int (cardinal (ce X)).
  move=> X XE ecx; split => // => coe.
  move: (even_odd_sum (cardinal (ce X)) (cardinal X)) => [_ ee _].
  by move: (ee coe ecx); rewrite csumC (ce2 _ XE); move => [].
move: (rep_i nne); set t:= rep E=> repe.
pose ut x := Yo (inc t x) (x -s1 t) (x +s1 t).
have uut: forall x, sub x E -> (ut (ut x)) = x.
  move => x xE; rewrite /ut; case: (inc_or_not t x) => tx; Ytac0.
    have nst: ~(inc t (x -s1 t)) by move /setC1_P => [].
    by Ytac0; rewrite setC1_K.
  have nst: inc t (x +s1 t) by apply /setU1_P; right.
  by Ytac0; apply /setU1_K.
have u1: forall x, sub x E -> sub (ut x) E.
  move => x xe s; rewrite /ut; Ytac st.
       by move => /setC_P [sx _]; apply: xe.
  by case /setU1_P; [ apply: xe | move => -> ].
exists (Lf (fun z => ut (ce z)) fs_even fs_odd);split; aw; apply: lf_bijective.
    move => s => /Zo_P [] /setP_P ta tb; apply /Zo_P; split.
      apply /setP_P; fprops.
    move: (ce_e _ ta tb) => ec; move:(fsx _ (u1 _ (cs1 s))).
    rewrite /ut; Ytac xt => cb.
      by move: (proj1 (even_odd_pred cb)); rewrite - (card_succ_pr2 xt); apply.
    by move: ((proj1 (even_odd_succ _) ec)); rewrite card_succ_pr.
  move => u v /Zo_P [] /setP_P ue _ /Zo_P [] /setP_P ve _ eq1.
  move: (f_equal ut eq1); rewrite (uut _ (cs1 _)) (uut _ (cs1 _)).
  by rewrite - {2} (cs4 _ ue) - {2} (cs4 _ ve) => ->.
move => y => /Zo_P [] /setP_P ta tb; move: (u1 _ ta) => ue.
exists (ce (ut y)) => //; last by rewrite (cs4 _ ue) (uut _ ta).
apply: Zo_i; [by apply /setP_P | apply: (ce_e _ ue) ].
move: (fsx _ ue); rewrite /ut; Ytac xt => cb.
  by move: (proj2 (even_odd_pred cb)); rewrite - (card_succ_pr2 xt); apply.
by move: ((proj2 (even_odd_succ _) tb)); rewrite card_succ_pr.
Qed.

Lemma Exercise5_3a n p: inc n Bnat -> inc p Bnat ->
  card_sumb (Bintc p)
     (fun k => (binom n k) *c (binom (n -c k) (p -c k)))
   = \2c ^c p *c binom n p.
Proof.
move => nB pB.
set E := Bint n.
set F :=subsets_with_p_elements p E.
have ce: cardinal E = n by apply:(card_Bint nB).
set rhs := \2c ^c p *c binom n p.
set EE := (powerset E \times powerset E).
set G1 := Zo EE (fun z => inc (P z) F /\ sub (Q z) (P z)).
have res1: cardinal G1 = rhs.
  pose phi := Lf P G1 F.
  have sp: G1 = source phi by rewrite /phi; aw.
  have tp: F = target phi by rewrite /phi; aw.
  rewrite /rhs (subsets_with_p_elements_pr nB pB ce) -/F tp sp cprodC.
  have lfa: lf_axiom P G1 F by move => t /Zo_P [_ []].
  have fphi: function phi by apply: lf_function.
  apply:(shepherd_principle fphi).
  move => x; rewrite - tp => xf.
  set K := inv_image_by_fun _ _.
  pose f := Lf (fun z => J x z) (powerset x) K.
  move /Zo_P: (xf) => [] /setP_P xE cx.
  have bf: bijection f.
    apply lf_bijective.
        move => y /setP_P yx.
        have aux: inc (J x y) G1.
          apply /Zo_P; aw;split => //; apply: setXp_i; apply /setP_P => //.
          apply: (sub_trans yx xE).
        apply :(iim_fun_set1_i fphi); rewrite /phi;aw.
      move => u v _ _ h; exact (pr2_def h).
    move => y /(iim_fun_set1_P _ fphi) []; rewrite - sp => yG.
    move /Zo_P: (yG) => [pa [pb pc]]; rewrite /phi; aw => ->; exists (Q y).
      by apply /setP_P.
    by rewrite (setX_pair pa).
  have : cardinal (source f) = cardinal (target f) by apply /card_eqP;exists f.
  rewrite /f;aw; rewrite card_setP - cx => <-.
  apply: cpow_pr; fprops.
set G2 := Zo EE (fun z => [/\ cardinal (P z) <=c p,
       cardinal (Q z) = p -c cardinal (P z) & sub (Q z) (E -s (P z))]).
have fse: finite_set E by red; rewrite /E(card_Bint nB); apply /BnatP.
have res2: cardinal G2 = rhs.
  rewrite - res1; symmetry; apply /card_eqP.
  exists (Lf (fun z => J (Q z) ((P z) -s (Q z))) G1 G2);split; aw.
  apply: lf_bijective.
      move => z /Zo_P [] /setX_P [pz Pz Qz] [pa pb]; apply /Zo_P; aw.
      move /Zo_P: pa => [_ pc].
      move /setP_P:Pz => pze; move: (sub_finite_set pze fse) => fsp.
      split; last split.
      by apply: setXp_i => //; apply /setP_P => t /setC_P [pa _]; apply: pze.
      by move: (sub_smaller pb); rewrite pc.
      by rewrite (cardinal_setC4 pb fsp) pc.
      by move /setP_P:Qz => qze t /setC_P [ta tb]; apply /setC_P;split;fprops.
    move => u v /Zo_P [pa [_ pb]] /Zo_P [pc [_ pd]] eq1.
    move: (pr1_def eq1) (pr2_def eq1) => eq2 eq3.
    rewrite - (setX_pair pa) - (setX_pair pc) - (setU2_Cr pb) - (setU2_Cr pd).
    by rewrite eq3 eq2.
  move => y /Zo_P [] /setX_P [pa Py Qy] [pb pc pd].
  have a0 : ((P y \cup Q y) -s P y) = Q y.
    set_extens t.
       move => /setC_P [] /setU2_P; case => //.
     move => tq; apply /setC_P;split;fprops => py.
     by move: (pd _ tq) => /setC_P; case.
  have aux: J (P y) ((P y \cup Q y) -s P y) = y by rewrite - {5} pa a0.
  move: (Py) Qy => /setP_P Py' /setP_P Qy.
  have a2: sub (P y) (P y \cup Q y) by move => t tp; fprops.
  have a3:inc (P y \cup Q y) (powerset E).
      by apply /setP_P => // t /setU2_P;case; fprops.
  exists (J (P y \cup Q y) (P y)); aw; last by rewrite a0 pa.
  apply /Zo_P; aw;split; first by apply: setXp_i.
  split => //;apply :Zo_i => //.
  rewrite (cardinal_setC2 a2) - csum2_pr2b a0 pc - csum2_pr2a.
  by apply: cdiff_pr.
pose Xk k := Zo EE (fun z => [/\ cardinal (P z) = k,
           cardinal (Q z) = p -c cardinal (P z) & sub (Q z) (E -s P z)]).
set X := Lg (Bintc p) Xk.
have X1: fgraph X by rewrite /X; fprops.
have X2: mutually_disjoint X.
  red;rewrite /X; bw => i j ip jp; bw;mdi_tac nij => u ua ub; case: nij.
  by move: ua ub => /Zo_hi [<- _ _] /Zo_hi [<- _ _].
have X3: (unionb X) = G2.
   rewrite /X;set_extens t.
     move /setUb_P; bw; move => [y yp]; bw; move /Zo_P => [p1 [p2 p3 p4]].
      by apply /Zo_i => //; rewrite p3 p2; split => //;apply /(BintcP pB).
   move /Zo_P=> [p1 [p2 p3 p4]]; apply /setUb_P; bw.
   by move /(BintcP pB): p2 => h; ex_tac; bw; apply /Zo_P.
move: (csum_pr4 X2); rewrite X3 res2 => ->.
rewrite /X; bw; rewrite /card_sumb; apply: f_equal; apply: Lg_exten.
move => k kp. move: (kp) => /(BintcP pB) kp1; bw.
set F1 := subsets_with_p_elements k E.
pose phi := Lf P (Xk k) F1.
have sp: (Xk k) = source phi by rewrite /phi; aw.
have tp: F1 = target phi by rewrite /phi; aw.
have kB: inc k Bnat by apply (BS_le_int kp1 pB).
rewrite (subsets_with_p_elements_pr nB kB ce) -/F1 tp sp.
have lfa: lf_axiom P (Xk k) F1.
  by move => t /Zo_P [] /setX_P [pa pb pc] [pd _ _]; apply: Zo_i.
have fphi: function phi by apply: lf_function.
symmetry;apply:(shepherd_principle fphi).
move => x; rewrite - tp => xf.
set K := inv_image_by_fun _ _.
move: (xf) => /Zo_P [] /setP_P xe cx.
have nkB: inc (n -c k) Bnat by fprops.
have pkB: inc (p -c k) Bnat by fprops.
have cdx:cardinal (E -s x) = n -c k by rewrite (cardinal_setC4 xe fse) cx ce.
rewrite (subsets_with_p_elements_pr nkB pkB cdx).
apply /card_eqP.
set K0 := (subsets_with_p_elements (p -c k) (E -s x)).
exists (Lf Q K (subsets_with_p_elements (p -c k) (E -s x))); split;aw.
have k0p: forall y, inc y K <-> [/\ inc y EE, P y = x & inc (Q y) K0].
  move =>t; apply: (iff_trans (iim_fun_set1_P x fphi t)).
  rewrite - sp /phi; split.
    move => [tk]; aw=> pt.
    move: tk => /Zo_P [te [p1 p2 p3]];split => //; apply/Zo_P.
    by rewrite -p1;split => //; apply /setP_P; rewrite pt.
   move => [p1 p2 p3]; suff: inc t (Xk k) by move =>h;aw.
   by move/ Zo_P: p3 => [] /setP_P sa sb; apply/ Zo_P; rewrite p2 cx.
apply: lf_bijective.
    by move => t /k0p [_ _].
  move => u v /k0p [u1 pu _]/k0p [v1 pv _] sv.
  by rewrite - (setX_pair u1) - (setX_pair v1) pu pv sv.
move => y yk0; exists (J x y); aw; apply /k0p; aw;split => //.
apply: setXp_i => //; apply /setP_P => //.
by move /Zo_P: yk0 => [] /setP_P h _ t ty; move /setC_P: (h _ ty) => [].
Qed.

Definition even_card_sub I := Zo (powerset I) (fun z => even_int (cardinal z)).
Definition even_card0_sub I := even_card_sub I -s1 emptyset.
Definition odd_card_sub I := Zo (powerset I) (fun z => odd_int (cardinal z)).

Lemma odd_nonempty x: odd_int (cardinal x) -> nonempty x.
Proof.
move => h; apply /nonemptyP => h1.
by move: h; rewrite h1 cardinal_set0; move => [_]; move: even_zero.
Qed.

Section Exercise5_5.
Variables (E r: Set) (f: Set -> Set).
Hypothesis lr:lattice r.
Hypothesis dl: distributive_lattice1 r.
Hypothesis sr: E = substrate r.
Hypothesis card_f: forall x, inc x E -> cardinalp (f x).
Hypothesis hyp_f: forall x y, inc x E -> inc y E ->
    (f x) +c (f y) = (f (sup r x y)) +c f (inf r x y).

Definition Exercise5_5_conc I :=
   f (supremum r I) +c
       card_sumb (even_card0_sub I) (fun z => f (infimum r z))
    = card_sumb (odd_card_sub I) (fun z => f (infimum r z)).
Definition Exercise5_5_conc_aux I g :=
  f (supremum r (fun_image I g)) +c
       card_sumb (even_card0_sub I) (fun z => f (infimum r (fun_image z g)))
    = card_sumb (odd_card_sub I) (fun z => f (infimum r (fun_image z g))).

Lemma Exercise5_5_a1 n g (I:=Bintc n):
   inc n Bnat -> (forall i, inc i I -> inc (g i) E) ->
   Exercise5_5_conc_aux I g.
Proof.
move => nB;rewrite /I; clear I; move: n nB g.
move: (proj1 lr) => or.
apply: cardinal_c_induction.
   rewrite Bint_cc00 /Exercise5_5_conc_aux; move =>g H.
   rewrite /card_sumb; set f1 := Lg _ _; set f2 := Lg _ _.
   have pA: domain f1 = emptyset.
      rewrite /f1; bw; apply /set0_P => s /Zo_P [] /Zo_P [] /setP_P p1 p2.
      move /set1_P => se; move: p2.
      have ->: s = (singleton \0c).
         apply: set1_pr1; first by apply /nonemptyP.
         by move => z zs; apply /set1_P; apply: p1.
      by rewrite cardinal_set1; move: odd_one => [].
   have pB: inc (singleton \0c) (odd_card_sub (singleton \0c)).
     apply /Zo_P; split; first by apply /setP_P; fprops.
     rewrite cardinal_set1; apply: odd_one.
   have pC: domain f2 = singleton (singleton \0c).
     rewrite /f2; bw; apply: set1_pr => //.
     move => z /Zo_P [] /setP_P pa pb.
     apply: set1_pr1; last by move => s sz; apply /set1_P; apply: pa.
     by apply: odd_nonempty.
   move: (funI_set1 g \0c) => pD.
   have pE: inc (g \0c) (substrate r) by rewrite - sr; apply: H; fprops.
   rewrite pD (supremum_singleton or pE).
   have pF: (Vg f2 (singleton \0c)) = (f (g \0c)).
     by rewrite /f2; bw; rewrite pD (infimum_singleton or pE).
   have pG: cardinalp ( (Vg f2 (singleton \0c))).
     rewrite pF; apply:card_f; apply: H; fprops.
   rewrite (csum_trivial pA) (csum_trivial1 pC pG) pF; aw.
   by rewrite -pF.
move => n nB Hrec g gse.
move: (BS_succ nB) => snB.
set I1 := (Bintc (succ n)).
set I := (Bintc n); set z := succ n.
have [pa pb]: I +s1 z = I1 /\ ~ inc z I.
    rewrite /I /I1 (Bint_co_cc nB) (Bint_co_cc snB); apply: (Bint_pr4 snB).
rewrite / Exercise5_5_conc_aux - {1} pa funI_setU1.
have gxsr: forall i, inc i I1 -> inc (g i) (substrate r) by ue.
have gzr: inc (g z) (substrate r) by apply: gxsr; apply/ BintcP; fprops.
have sii': sub I I1 by rewrite -pa => t ti; fprops.
have fsI1: finite_set I1 by apply /BnatP; rewrite card_Bintc; fprops.
have fsI: finite_set I by apply /BnatP; rewrite card_Bintc.
pose g' x := inf r (g x) (g z).
have g'xsr: forall x, inc x I1 -> inc (g' x) (substrate r).
   move: (lattice_props lr) => [p1 [p2 _]].
   by move => x xI; apply: (p2 _ _ (gxsr _ xI) gzr).
have sr1: forall s, sub s I1 -> sub (fun_image s g) (substrate r).
  by move => s si t /funI_P [u us ->];apply: gxsr; apply: si.
have sr1': forall s, sub s I1 -> sub (fun_image s g') (substrate r).
  by move => s si t /funI_P [u us ->]; apply: g'xsr; apply: si.
have fs1: forall s, sub s I1 -> finite_set (fun_image s g).
   move => s si; apply: finite_fun_image; apply: (sub_finite_set si fsI1).
have fs1': forall s, sub s I1 -> finite_set (fun_image s g').
  move => s si; apply: finite_fun_image; apply: (sub_finite_set si fsI1).
have rec1:
   (inf r (supremum r (fun_image I g)) (g z)) = supremum r (fun_image I g').
  move: (proj1 (Exercise1_16a lr)) => h.
  move: (proj33 (Exercise1_16b lr)) => h1.
  move: (h1 (h dl)) => dl2; clear h h1.
  have dl2': forall a b, inc a E -> inc b E ->
    inf r (sup r a b) (g z) = sup r (inf r a (g z)) (inf r b (g z)).
    by rewrite sr;move => a b ae be; rewrite inf_C dl2 // inf_C (inf_C r b).
  suff: forall m, inc m Bnat -> m <=c n ->
      inf r (supremum r (fun_image (Bintc m) g)) (g z) =
        supremum r (fun_image (Bintc m) g').
      move => aux; apply: (aux n nB); fprops.
  apply: cardinal_c_induction.
    move => h; rewrite Bint_cc00 (funI_set1 g \0c) (funI_set1 g' \0c).
    have oi: inc \0c I1 by apply:sii';apply /(BintcP nB).
    have aa: inc (g \0c) (substrate r) by apply: gxsr.
    by rewrite supremum_singleton //supremum_singleton //; apply: g'xsr.
  move => m mB Hrec1 smn; move: (BS_succ mB) => smB.
  move: (proj1 (Bint_pr4 smB)).
  have sim: inc (succ m) I1 by apply: sii';apply /(BintcP nB).
  move: (card_le_succ mB) => lemsm; move: (card_leT lemsm smn) => le3.
  rewrite - (Bint_co_cc mB) - (Bint_co_cc smB); move => <-.
  have smI: sub (Bintc m) I1.
     move => t /(BintcP mB)=> tb; apply: sii'; apply /(BintcP nB).
     by apply: (card_leT tb le3).
  move: (sr1 _ smI) (sr1' _ smI)(fs1 _ smI) (fs1' _ smI) => sa sa' sc sc'.
  have sb: nonempty (fun_image (Bintc m) g).
     exists (g m); apply /funI_P; exists m => //; apply /BintcP; fprops.
  have sb': nonempty (fun_image (Bintc m) g').
     exists (g' m); apply /funI_P; exists m=> //; apply /BintcP; fprops.
  have sd: inc (g (succ m)) (substrate r) by apply: gxsr.
  have sd': inc (g' (succ m)) (substrate r) by apply: g'xsr.
  have se: inc (supremum r (fun_image (Bintc m) g)) (substrate r).
    by apply: (inc_supremum_substrate or sa); apply: lattice_finite_sup2.
  rewrite 2!funI_setU1 sup_setU1 // sup_setU1 // - (Hrec1 le3).
  by rewrite inf_C dl2 // inf_C (inf_C _ (g z)) -/(g' (succ m)).
have inf_gp: forall s, sub s I -> nonempty s ->
  infimum r (fun_image (s +s1 z) g) = (infimum r (fun_image s g')).
  move => s sa sb.
  have fs: finite_set s by apply: (sub_finite_set sa fsI).
  pose b s := infimum r (fun_image (s +s1 z) g) = infimum r (fun_image s g').
  pose a s := sub s I.
  have p1: forall u, a (singleton u) -> b (singleton u).
     move => u h; rewrite /b funI_setU1 2! funI_set1.
     have ui: inc u I1 by apply: sii';apply:h; fprops.
     rewrite (infimum_singleton or (g'xsr _ ui)) setU2_11 //.
  apply:(finite_set_induction2 p1 _ fs) => //.
  move => u v h neu; rewrite /a /b => ra.
  have vi1: inc v I1 by apply: sii'; apply: ra; fprops.
  have gvr: inc (g v) (substrate r) by apply (gxsr _ vi1).
  have gvr': inc (g' v) (substrate r) by apply (g'xsr _ vi1).
  have ->: ((u +s1 v) +s1 z) = (((u +s1 z) +s1 v) +s1 z).
    rewrite - 3!setU2_A (setU2_C _ (singleton z)).
    by rewrite (setU2_A (singleton z)) setU2_id.
  have au: a u by move => t tu;apply: ra; fprops.
  have ne1: nonempty (fun_image ((u +s1 z) +s1 v) g).
      exists (g v); apply: funI_i; fprops.
  have ne2: nonempty (fun_image (u +s1 z) g).
     exists (g z); apply: funI_i; fprops.
  have ne3: nonempty (fun_image u g').
    move:neu => [t tu]; exists (g' t); apply: funI_i; fprops.
  have aux1: sub ((u +s1 z) +s1 v) I1.
     move => t; case /setU1_P; last by move => ->.
     case /setU1_P; first by move => tu;apply: sii'; apply: au.
     move => ->; apply /(BintcP snB); fprops.
  have aux2: sub (u +s1 z) I1 by move => t ts; apply: aux1; apply/setU1_P; left.
  have aux3: sub u I1 by move => t ts; apply: sii'; apply: au.
  have aux4:inc (infimum r (fun_image (u +s1 z) g)) (substrate r).
    apply: (inc_infimum_substrate or (sr1 _ aux2)).
    apply: (lattice_finite_inf2 lr (fs1 _ aux2) (sr1 _ aux2) ne2).
  rewrite funI_setU1 (inf_setU1 lr (sr1 _ aux1) ne1 (fs1 _ aux1) gzr).
  rewrite funI_setU1 (inf_setU1 lr (sr1 _ aux2) ne2 (fs1 _ aux2) gvr).
  move: (lattice_props lr) => [_ [ _ [_ [_ [_ [idr _]]]]]].
  rewrite - (idr _ _ _ aux4 gvr gzr) -/(g' v) (h au neu).
  by rewrite funI_setU1 (inf_setU1 lr (sr1' _ aux3) ne3 (fs1' _ aux3) gvr').
have gIr: sub (fun_image I g) (substrate r) by apply: sr1.
have gIhs: has_supremum r (fun_image I g).
   apply: lattice_finite_sup2 => //; first by apply: finite_fun_image.
   exists (g n); apply : funI_i; apply/ BintcP; fprops.
move : (inc_supremum_substrate or gIr gIhs); rewrite - sr => sIE.
have pc: forall i, inc i I -> inc (g i) E.
   by rewrite sr => i iI; apply:gxsr; apply: sii'.
have pd: forall i, inc i I -> inc (g' i) E.
   by rewrite sr => i iI; apply:g'xsr; apply: sii'.
move: (Hrec _ pc) (Hrec _ pd);rewrite / Exercise5_5_conc_aux.
set seG := card_sumb _ _;set soG := card_sumb _ _.
set seG' := card_sumb _ _;set soG' := card_sumb _ _.
set seI := card_sumb _ _; set soI := card_sumb _ _.
set X := f _; set X':= f _; set X'' := f _.
move => r1 r2.
move: (gzr); rewrite - sr => gzE.
move: (hyp_f sIE gzE); rewrite rec1 - (supremum_setU1 lr gIr gIhs gzr).
move => auxx.
set ff := (fun t => t +s1 z).
clear gIr gIhs sIE pc pd gzE.
have ->: seI = seG +c soG'.
  set A := even_card0_sub I;
  set B := fun_image (odd_card_sub I) ff.
  have dAB: disjoint A B.
     apply: disjoint_pr => u /Zo_P [] /Zo_P [] /setP_P ra rb rc /funI_P.
     move => [t _ h]; case: pb; apply: ra; rewrite h /ff; fprops.
  have uAB: (even_card0_sub I1) = A \cup B.
     rewrite /B/ff;set_extens t.
       move => /Zo_P [] /Zo_P [] /setP_P ra rb te; apply /setU2_P.
       case: (inc_or_not z t) => zt.
         right; apply /funI_P; exists (t -s1 z);last by rewrite (setC1_K zt).
         apply /Zo_P; split.
           apply /setP_P => s /setC1_P [st sz];move: (ra _ st); rewrite -pa.
           by case /setU1_P.
         move: (card_succ_pr2 zt) => e1.
         split; first by apply:BS_nsucc; fprops;rewrite -e1; exact (proj1 rb).
         move => ec; move: (proj1 (even_odd_succ _) ec).
         rewrite- (card_succ_pr2 zt); by case.
       left; apply /Zo_P;split => //; apply /Zo_P;split => //; apply /setP_P.
       move => s st;move: (ra _ st); rewrite -pa;case /setU1_P => //.
       by move => sz; case: zt; rewrite - sz.
    case /setU2_P.
      move => /Zo_P [] /Zo_P [] /setP_P ra rb rc; apply/Zo_P;split => //.
      apply /Zo_P;split => //; apply /setP_P; rewrite -pa => s st.
      by apply /setU1_P; left; apply: ra.
    move /funI_P => [s ] /Zo_P [] /setP_P sa sb ->; apply/ Zo_P.
    split; last by apply /set1_P;apply /nonemptyP; exists z; fprops.
    apply /Zo_P; split; first by apply /setP_P; rewrite -pa; apply:setU2_S2.
    have zs: ~ inc z s by move => h; case: pb; apply: sa.
    rewrite (card_succ_pr zs); apply: (proj2 (even_odd_succ _) sb).
  move: (csumA_setU2 (fun z => f (infimum r (fun_image z g))) dAB).
  suff: card_sumb B (fun s => f (infimum r (fun_image s g))) = soG'.
      by move => ->; rewrite - uAB.
   rewrite /card_sumb.
   set f1 := Lf ff (odd_card_sub I) B.
   have pc: lf_axiom ff (odd_card_sub I) B.
     by move => s sa; apply: funI_i.
   have fb: bijection f1.
     apply: lf_bijective => //.
         move => u v /Zo_P [] /setP_P ui _ /Zo_P [] /setP_P vi _ sv.
         have nzu: ~ (inc z u) by move => b; apply: pb; apply: ui.
         have nzv: ~ (inc z v) by move => b; apply: pb; apply: vi.
         by rewrite - (setU1_K nzu) -/(ff _) sv (setU1_K nzv).
      by move => y /funI_P.
   have ff1: function f1 by fct_tac.
   set XX := Lg B _.
   have fgxx: fgraph XX by rewrite /XX; fprops.
   have tf1: target f1 = domain XX by rewrite /f1 /XX; aw; bw.
   rewrite (csum_Cn tf1 fb) /soG' /f1/card_sumb/composef; aw.
   apply: f_equal; apply: Lg_exten => s sa.
   move /Zo_P: (sa) => [] /setP_P sb sc.
   have rb: inc (s +s1 z) B by apply: pc.
   rewrite -/(Vf _ _); aw; rewrite /XX; bw; rewrite inf_gp //.
   by apply:odd_nonempty.
have ->: soI = soG +c seG' +c (f (g z)).
  rewrite /soI /soG /seG' -/I.
  set A := odd_card_sub I;
  set B := fun_image (even_card_sub I) ff.
  have dAB: disjoint A B.
     apply: disjoint_pr => u /Zo_P [] /setP_P ra rb /funI_P.
     move => [t _ h]; case: pb; apply: ra; rewrite h /ff; fprops.
  have uAB: (odd_card_sub I1) = A \cup B.
    set_extens t.
      move => /Zo_P []/setP_P ra rb; apply /setU2_P.
      case: (inc_or_not z t) => zt.
        right;apply /funI_P; exists (t -s1 z); last by rewrite /ff (setC1_K zt).
        apply /Zo_P; split.
          apply /setP_P => s /setC1_P [st sz];move: (ra _ st); rewrite -pa.
          by case /setU1_P.
        move: (card_succ_pr2 zt) => e1; ex_middle bad.
        have oi: odd_int (cardinal (t -s1 z)).
          split => //; apply:BS_nsucc; fprops;rewrite -e1; exact (proj1 rb).
        by move: (proj2 (even_odd_succ _) oi); rewrite - e1 => h; case: rb.
        left; apply /Zo_P;split => //; apply /setP_P.
      move => s st;move: (ra _ st); rewrite -pa;case /setU1_P => //.
      by move => sz; case: zt; rewrite - sz.
    case /setU2_P.
      move => /Zo_P [] /setP_P ra rb; apply/Zo_P;split => //; apply /setP_P.
      apply: (sub_trans ra sii').
    move /funI_P => [s] /Zo_P [] /setP_P sa sb ->; apply/ Zo_P.
    split;first by apply /setP_P; rewrite -pa; apply:setU2_S2.
    have zs: ~ inc z s by move => h; case: pb; apply: sa.
    rewrite (card_succ_pr zs); apply: (proj1 (even_odd_succ _) sb).
  move: (csumA_setU2 (fun z => f (infimum r (fun_image z g))) dAB).
  rewrite uAB => ->; rewrite - csumA; congr (_ +c _).
  rewrite /B.
  have ->: even_card_sub I = even_card0_sub I +s1 emptyset.
    set_extens t.
       move => h; apply /setU1_P;case: (emptyset_dichot t) => sd; first by right.
       by left; apply /Zo_P; split => //; move /set1_P; apply /nonemptyP.
    case /setU1_P; [ by move /Zo_P => [] | move => ->; apply /Zo_P].
    split; first by apply: setP_0i.
    by rewrite cardinal_set0; apply: even_zero.
  have di2: disjoint (fun_image (even_card0_sub I) ff)
     (singleton (singleton z)).
     apply: disjoint_pr => u /funI_P [v] /Zo_P [] /Zo_P [sa sb].
     move /set1_P => vne eq1 /set1_P uz; move: sb.
     have ->: v = singleton z.
        apply : set1_pr1; first by apply /nonemptyP.
        move => t tv; apply /set1_P; rewrite -uz eq1 /ff; fprops.
    rewrite cardinal_set1; exact (proj2 odd_one).
  rewrite /ff funI_setU1 set0_U2 (csumA_setU2 _ di2).
  rewrite {2} /card_sumb; set f2 := Lg _ _.
  have sid: domain f2 = (singleton (singleton z)) by rewrite /f2; bw.
  have eq1: Vg f2 (singleton z) = f (g z).
      rewrite /f2; bw;[ rewrite funI_set1 infimum_singleton // | fprops].
  have cf1: cardinalp (Vg f2 (singleton z)) by rewrite eq1; apply: card_f; ue.
  rewrite (csum_trivial1 sid cf1) eq1 csumC (csumC _ (f (g z))); apply:f_equal.
  set B1:= fun_image _ _.
  set f1 := Lf ff (even_card0_sub I) B1.
   have pc: lf_axiom ff (even_card0_sub I) B1.
     by move => s sa; apply: funI_i.
   have fb: bijection f1.
     apply: lf_bijective => //.
       move => u v /Zo_P [] /Zo_P [] /setP_P ui _ _.
       move => /Zo_P [] /Zo_P [] /setP_P vi _ _ sv.
       have nzu: ~ (inc z u) by move => b; apply: pb; apply: ui.
       have nzv: ~ (inc z v) by move => b; apply: pb; apply: vi.
       by rewrite - (setU1_K nzu) -/(ff _) sv (setU1_K nzv).
     by move => y /funI_P.
   have ff1: function f1 by fct_tac.
   rewrite /card_sumb; set XX := Lg B1 _.
   have fgxx: fgraph XX by rewrite /XX; fprops.
   have tf1: target f1 = domain XX by rewrite /f1 /XX; aw; bw.
   rewrite (csum_Cn tf1 fb) /soG' /f1/card_sumb/composef; aw.
   apply: f_equal; apply: Lg_exten => s sa.
   have rb: inc (s +s1 z) B1 by apply: pc.
   move /Zo_P: (sa) => [] /Zo_P [] /setP_P sb sc /set1_P sd.
   rewrite -/(Vf _ _); aw; rewrite /XX; bw; rewrite inf_gp //.
   by apply/nonemptyP.
rewrite -r2 -r1 (csumA seG) (csumC seG) 2!csumA.
rewrite -auxx -/X.
by rewrite - (csumA X) (csumC (f (g z))) csumA - csumA (csumC (f (g z))) csumA.
Qed.

Lemma Exercise5_5_a2 I: sub I E -> nonempty I -> finite_set I ->
   Exercise5_5_conc I.
Proof.
move => IE neI fsi.
set m := cardinal I.
have mB: inc m Bnat by rewrite /m; apply /BnatP.
have mz: m <> \0c.
   move => mz; move: neI;rewrite (cardinal_nonemptyset mz).
  by case /nonemptyP.
move: (card_Bintcp mB mz); move /card_eqP.
move: (cpred_pr mB mz) => [pa pb].
move => [G [bG sG tG]].
have fg: function G by fct_tac.
set K := Bintc (cpred m).
pose g x := Vf G x.
have aux: forall x, inc x K -> inc (g x) E.
  rewrite /K - sG; move => x xk; apply: IE; rewrite - tG /g; Wtac.
move: (Exercise5_5_a1 pa aux).
rewrite /Exercise5_5_conc_aux /Exercise5_5_conc.
have ->:(fun_image (Bintc (cpred m)) g) = I.
  rewrite - sG - tG;set_extens t.
     move /funI_P; rewrite /g; move => [z za ->]; Wtac.
   move => tg; move: (bij_surj bG tg) => [x xs <-].
   apply /funI_P; ex_tac.
rewrite /card_sumb; set s1 := card_sum _; set s2 := card_sum _.
set s3 := card_sum _; set s4 := card_sum _.
have ga: forall t, sub t (source G) -> sub (fun_image t g) I.
   move => t tg s /funI_P [z zt ->]; rewrite -tG /g; Wtac.
have gb: forall t, sub t (source G) ->
   cardinal t = cardinal (fun_image t g).
   move => t tg; apply /card_eqP.
   exists (Lf g t (fun_image t g)); split;aw; apply /lf_bijective.
       move=> s sa; apply /funI_P; ex_tac.
     move => u v ut vt sg; move: (tg _ ut) (tg _ vt) => ug vg.
     apply: (bij_inj bG ug vg sg).
   by move => y /funI_P.
have gc: forall u v, sub u (source G) -> sub v (source G) ->
   fun_image u g = fun_image v g -> u = v.
   move => u v us vs sf; set_extens t => tu.
     have : inc (g t) (fun_image v g) by rewrite - sf; apply: funI_i.
     move /funI_P => [z za zb].
     by rewrite (bij_inj bG (us _ tu)(vs _ za) zb).
   have : inc (g t) (fun_image u g) by rewrite sf; apply: funI_i.
   move /funI_P => [z za zb].
   by rewrite (bij_inj bG (vs _ tu) (us _ za) zb).
have gd: forall u, sub u I -> exists2 t, sub t (source G)& (fun_image t g) =u.
   move => u uI; exists (Zo (source G) (fun z => inc (g z) u)).
      by apply: Zo_S.
   set_extens t; first by move => /funI_P [z ] /Zo_P [] _ h ->.
   rewrite -tG in uI; move => tu; move: (bij_surj bG (uI _ tu)) => [x p1 p2].
   apply /funI_P; rewrite -p2 /g; exists x => //; apply: Zo_i => //; ue.
have ->: s1 = s3.
  rewrite /s1 /s3 - sG.
  set A1 := even_card0_sub _; set A2 := even_card0_sub _.
  set X := Lg A2 _.
  set h := Lf (fun z => (fun_image z g)) A1 A2.
  have pc: fgraph X by rewrite /X; fprops.
  have pd: target h = domain X by rewrite /h /X; bw; aw.
  have ta: lf_axiom (fun_image^~ g) A1 A2.
    move => t /Zo_P [] /Zo_P [] /setP_P t1 t2 /set1_P te.
    apply /Zo_P; split.
        apply /Zo_P; split; first by apply /setP_P; fprops.
        by rewrite - (gb _ t1).
    apply /set1_P => e; case: (emptyset_dichot t) => //; move => [s st].
    by empty_tac1 (g s); apply: funI_i.
  have pe: bijection h.
     apply: lf_bijective => //.
         move => u v /Zo_P [] /Zo_P [] /setP_P h1 _ _.
         by move => /Zo_P [] /Zo_P [] /setP_P h2 _ _; apply: gc.
       move => y /Zo_P [] /Zo_P [] /setP_P p1 p2 p3.
       move: (gd _ p1) => [t t1 t2]; exists t => //.
       apply /Zo_P; split.
          apply /Zo_P; split; first by apply/setP_P.
          by rewrite (gb _ t1) t2.
       move /set1_P => h1; case: p3; apply /set1_P; rewrite -t2.
       by rewrite h1; apply /set0_P => s /funI_P [z] /in_set0.
  have pf: function h by fct_tac.
  rewrite (csum_Cn pd pe) /composef {1} /h; aw; apply: f_equal.
  apply: Lg_exten => t tb; rewrite -/(Vf h t) /h; aw; rewrite /X; bw.
  by apply: ta.
have -> //: s2 = s4.
rewrite /s2 /s4 - sG.
set A1 := odd_card_sub _; set A2 := odd_card_sub _.
set X := Lg A2 _.
set h := Lf (fun z => (fun_image z g)) A1 A2.
have pc: fgraph X by rewrite /X; fprops.
have pd: target h = domain X by rewrite /h /X; bw; aw.
have ta: lf_axiom (fun_image^~ g) A1 A2.
   move => t /Zo_P [] /setP_P p1 p2; apply /Zo_P;rewrite - (gb _ p1);split=> //.
   apply /setP_P; fprops.
have pe: bijection h.
  apply lf_bijective => //.
     by move => u v /Zo_P [] /setP_P us _ /Zo_P [] /setP_P vs _; apply: gc.
   move => y /Zo_P [] /setP_P p1 p2; move: (gd _ p1) => [t t1 t2].
   exists t => //; apply /Zo_P; split; first by apply /setP_P.
   by rewrite (gb _ t1) t2.
have pf: function h by fct_tac.
rewrite (csum_Cn pd pe) /composef {1} /h; aw; apply: f_equal.
apply: Lg_exten => t tb; rewrite -/(Vf h t) /h; aw; rewrite /X; bw.
by apply: ta.
Qed.

End Exercise5_5.

Lemma setP_lattice_d1 A (r := subp_order A): distributive_lattice1 r.
Proof.
rewrite /distributive_lattice1 (proj2 (subp_osr A)) => x y z xA yA zA.
rewrite (proj1 (setP_lattice_pr xA yA)) (proj1 (setP_lattice_pr xA zA)).
rewrite (proj2 (setP_lattice_pr yA zA)).
move: (xA)(yA)(zA) => /setP_P xA' /setP_P yA' /setP_P zA'.
have yzA: inc (y \cap z) (powerset A).
  by apply /setP_P => t /setI2_P [ty _]; apply: yA'.
have xyA: inc (x \cup y) (powerset A).
  apply /setP_P => t /setU2_P; case => h; [by apply: xA' | by apply: yA'].
have xzA: inc (x \cup z) (powerset A).
  apply /setP_P => t /setU2_P; case => h; [by apply: xA' | by apply: zA'].
rewrite (proj1 (setP_lattice_pr xA yzA)) (proj2 (setP_lattice_pr xyA xzA)).
by rewrite set_UI2r.
Qed.

Lemma Exercise5_5_b1 x y:
  cardinal x +c cardinal y = cardinal (x \cup y) +c cardinal (x \cap y).
Proof.
have di: disjoint (x -s y) (x \cap y).
  by apply: disjoint_pr => u /setC_P [_ pa] /setI2_P [].
move: (csum2_pr5(set_I2Cr x y)); rewrite setU2Cr2 setU2_C => ->.
rewrite csum2_pr2b csum2_pr2b - csumA - (csum2_pr5 di).
by rewrite - setCC_r setC_v setC_0 csumC.
Qed.

Lemma Exercise5_5_b3 I (f: Set -> Set) : finite_set I ->
  cardinal (unionf I f) +c
       card_sumb (even_card0_sub I) (fun z => cardinal (intersectionf z f))
    = card_sumb (odd_card_sub I) (fun z => cardinal (intersectionf z f)).
Proof.
case: (emptyset_dichot I).
    move => ->; rewrite setUf_0 cardinal_set0.
    have ->: (even_card0_sub emptyset) = emptyset.
      by apply /set0_P => t /Zo_P [] /Zo_P [] /setP_P /sub_set0 h _ /set1_P.
    have ->: (odd_card_sub emptyset) = emptyset.
      apply /set0_P => t /Zo_P [] /setP_P/sub_set0 => te oi.
      by move: (odd_nonempty oi); move /nonemptyP; case.
    rewrite /card_sumb csum_trivial; aw; fprops; bw.
move => neI fse.
set m := cardinal I.
have mB: inc m Bnat by apply/BnatP.
have mz: m <> \0c.
   by move => h; move: (cardinal_nonemptyset h); apply /nonemptyP.
move: (card_Bintcp mB mz); move /card_eqP.
move: (cpred_pr mB mz); set n := cpred m; move=> [pa pb] [G [bG sG tG]].
have fg: function G by fct_tac.
pose g i := f (Vf G i).
set A := unionf I f; set E := powerset A;set r:= subp_order A.
have esr: E = substrate r by symmetry; apply: (proj2 (subp_osr A)).
have lr: lattice r by apply: setP_lattice.
move: (@setP_lattice_d1 A) => dl1.
have cf: forall x, inc x E -> cardinalp (cardinal x) by move => x xA; fprops.
have fp: forall x y, inc x E -> inc y E ->
     cardinal x +c cardinal y = cardinal (sup r x y) +c cardinal (inf r x y).
  move => x y xe ye; move: (setP_lattice_pr xe ye) => [-> ->].
  apply: Exercise5_5_b1.
have pc: (forall i, inc i (Bintc n) -> inc (g i) E).
  rewrite - sG => i iG; move: (Vf_target fg iG); rewrite tG => h.
  rewrite /g; apply /setP_P => s sa; apply /setUf_P; ex_tac.
move: (Exercise5_5_a1 lr dl1 esr cf fp pa pc).
rewrite /Exercise5_5_conc_aux.
set J := (Bintc n).
have pd: sub (fun_image J g) (powerset A).
   by move => t /funI_P [z za zb]; move: (pc _ za); rewrite zb.
move: (setU_sup pd) => h; rewrite - (supremum_pr2 (proj1 lr) h).
have pe: forall x, sub x J -> (fun_image x g) = fun_image (image_by_fun G x) f.
   rewrite /J - sG; move => x xJ.
    set_extens t => /funI_P [z za ->]; apply /funI_P.
      exists (Vf G z) => //; apply/ (Vf_image_P fg xJ); ex_tac.
    move /(Vf_image_P fg xJ): za => [u ux ->]; ex_tac.
have ->: (fun_image J g) = fun_image I f.
  by rewrite -tG - (surjective_pr0 (proj2 bG)) /image_of_fun sG; apply: pe.
have ->: union (fun_image I f) = A.
  set_extens t.
     move /setU_P => [z tz] /funI_P [u ui uv]; apply /setUf_P; ex_tac; ue.
  by move/setUf_P => [y yi tf]; apply /setU_P; exists (f y) => //; apply:funI_i.
have pf: forall x, inc x (powerset J) -> nonempty x ->
  (infimum r (fun_image x g)) = intersectionf (image_by_fun G x) f.
  move => x /setP_P qa qb.
  have ta: nonempty (fun_image x g) by apply: funI_setne.
  have tb: sub (fun_image x g) (powerset A).
     by move => t /funI_P [z zx ->]; apply: pc; apply: qa.
  move: (ta); rewrite {1} (pe _ qa) => ta1.
  have tc: nonempty (image_by_fun G x).
    apply /nonemptyP => ba; move: ta1; rewrite ba funI_set0.
    by case/nonemptyP.
  move: (setI_inf tb); Ytac0 => h1; rewrite - (infimum_pr2 (proj1 lr) h1).
  rewrite (pe _ qa); set_extens t.
      move /(setI_P ta1) => hi;apply: (setIf_i tc) => j ja.
      by apply: hi; apply: funI_i.
  move /(setIf_P _ tc) => hi;apply: (setI_i ta1) => j /funI_P [z za ->].
  by apply: hi.
have pg: forall s, sub s J -> sub (image_by_fun G s) I.
   by rewrite -tG; move => s sj; apply: fun_image_Starget1.
have ph: forall s, sub s J -> cardinal (image_by_fun G s) = cardinal s.
  move => s sj; symmetry;apply /card_eqP.
  apply equipotent_restriction1;[ ue | exact (proj1 bG)].
have pi: forall u v, sub u J -> sub v J ->
    image_by_fun G u = image_by_fun G v -> u = v.
  rewrite /J - sG; move => u v uJ vJ si; set_extens t => tu.
     have : inc (Vf G t) (image_by_fun G v).
       rewrite - si; apply /(Vf_image_P fg uJ); ex_tac.
     move /(Vf_image_P fg vJ) => [w wv] sv.
     by rewrite (bij_inj bG (uJ _ tu) (vJ _ wv) sv).
    have : inc (Vf G t) (image_by_fun G u).
       rewrite si; apply /(Vf_image_P fg vJ); ex_tac.
     move /(Vf_image_P fg uJ) => [w wv] sv.
     by rewrite (bij_inj bG (vJ _ tu)(uJ _ wv) sv).
have pj: forall y, inc y (powerset I) -> exists x,
    [/\ inc x (powerset J), image_by_fun G x = y & cardinal x = cardinal y].
  move => y /setP_P; rewrite - tG => yG; rewrite /J - sG.
  set x := Zo (source G) (fun z => inc (Vf G z) y).
  have xj: sub x (source G) by apply: Zo_S.
  have xj': sub x J by rewrite /J - sG.
  exists x; rewrite - (ph _ xj').
  have -> : image_by_fun G x = y.
   set_extens t.
     by move /(Vf_image_P fg xj) => [u] /Zo_P [_] hh ->.
    move => ty; apply /(Vf_image_P fg xj); move: (bij_surj bG (yG _ ty)).
    move => [a ag eq]; exists a => //; apply /Zo_P; rewrite eq;split => //.
  by split => //; apply /setP_P.
clear h.
rewrite /card_sumb; set x1 := card_sum _; set x2 := card_sum _.
set x3 := card_sum _; set x4 := card_sum _.
have [-> -> //]: x1 = x3 /\ x2 = x4; split.
   rewrite /x1 /x3.
   set A1 := even_card0_sub _; set A2 := even_card0_sub _.
   set X := Lg A2 _.
   set h := Lf (image_by_fun G) A1 A2.
   have qc: fgraph X by rewrite /X; fprops.
   have qd: target h = domain X by rewrite /X /h; bw; aw.
   have qb: lf_axiom (image_by_fun G) A1 A2.
     move => s /Zo_P [] /Zo_P [] /setP_P sj a1 /set1_P a2.
     move: (pg _ sj) (ph _ sj) => s1 s2.
     apply /Zo_P; split.
       by apply /Zo_P;rewrite s2;split => //; apply/setP_P.
     move /set1_P => s3; case: (emptyset_dichot s) => // [] [t ts].
     empty_tac1 (Vf G t); apply /Vf_image_P => //; [ ue | ex_tac].
  have qe: bijection h.
    apply: lf_bijective => //.
        move => u v /Zo_P [] /Zo_P [] /setP_P uJ _ _.
        by move => /Zo_P [] /Zo_P [] /setP_P vJ _ _; apply: pi.
    move => t /Zo_P [] /Zo_P [t1 t2] /set1_P t3.
    move: (pj _ t1) => [x [x5 x6 x7]].
    exists x => //; apply /Zo_P; split; first by apply /Zo_P; rewrite x7.
      by move /set1_P => xe; move: x6; rewrite xe fun_image_set0; apply: nesym.
  have qf: function h by fct_tac.
  rewrite (csum_Cn qd qe) /composef /h; aw; apply: f_equal.
  apply: Lg_exten => s sa; move: (qb _ sa) => qg.
  move /Zo_P: (sa) => [] /Zo_P [sb sc] /set1_P sd.
  by rewrite -/(Vf _ _) /X; aw; bw; rewrite pf //; apply /nonemptyP.
rewrite /x2 /x4.
set A1 := odd_card_sub _; set A2 := odd_card_sub _.
set X := Lg A2 _.
set h := Lf (image_by_fun G) A1 A2.
have qc: fgraph X by rewrite /X; fprops.
have qd: target h = domain X by rewrite /X /h; bw; aw.
have qb: lf_axiom (image_by_fun G) A1 A2.
  move => s /Zo_P [] /setP_P sj a1; move: (pg _ sj) (ph _ sj) => s1 s2.
  by apply /Zo_P; rewrite s2;split => //; apply/setP_P.
have qe: bijection h.
  apply /lf_bijective => //.
    by move => u v /Zo_P [] /setP_P uJ _ /Zo_P [] /setP_P vJ _; apply: pi.
  move => y /Zo_P [t1 t2]; move: (pj _ t1) => [x [x5 x6 x7]].
  exists x => //; apply /Zo_P; rewrite x7;split => //.
have qf: function h by fct_tac.
rewrite (csum_Cn qd qe) /composef /h; aw; apply: f_equal.
apply: Lg_exten => s sa; move: (qb _ sa) => qg.
move /Zo_P: (sa) => [sc sd]; move: (odd_nonempty sd) => nes.
by rewrite -/(Vf _ _) /X; aw; bw; rewrite pf.
Qed.

Lemma Exercise5_5_b2 I: finite_set I ->
  cardinal (union I) +c
       card_sumb (even_card0_sub I) (fun z => cardinal (intersection z))
    = card_sumb (odd_card_sub I) (fun z => cardinal (intersection z)).
Proof.
move => h.
move: (Exercise5_5_b3 id h).
rewrite - setU_prop /card_sumb; set s1 := Lg _ _; set s2 := Lg _ _.
set s3 := Lg _ _; set s4 := Lg _ _.
have ->: s1 = s3 by apply: Lg_exten => t; rewrite setI_prop.
have -> //: s2 = s4 by apply: Lg_exten => t; rewrite setI_prop.
Qed.


Lemma Exercise5_6 n h (I := (Bintc h))
    (f := fun i => (binom h i) *c (binom (n +c h -c i) h)):
   inc n Bnat -> inc h Bnat ->
   card_sumb (Zo I even_int) f = \1c +c card_sumb (Zo I odd_int) f.
Proof.
move => nB hB; rename f into f'.
set A := (Zo I even_int).
have za: inc \0c A by apply Zo_i; [apply/BintcP; fprops | apply: even_zero].
have nzc: ~ inc \0c (A -s1 \0c) by move /setC1_P => [].
have fc0: cardinalp (f' \0c) by rewrite /f'; fprops.
have nhB: inc (n +c h) Bnat by fprops.
rewrite - (setC1_K za) (csumA_setU1 _ nzc) {2} /f' (binom0 hB) (cdiff_n_0 nhB).
set J := (Bint h).
pose Ak k := graphs_sum_le J k.
pose Bk i := Zo (Ak n) (fun z => Vg z i <> \0c).
have cJ: cardinal J = h by rewrite card_Bint.
have fsj: finite_set J by apply /BnatP; rewrite cJ.
have r1: forall z (k:= cardinal z), sub z J -> nonempty z ->
    cardinal (intersectionf z Bk) = binom ((n +c h) -c k) h.
   move => z k zj nez.
   have ->: (intersectionf z Bk) =
      Zo (Ak n) (fun f => forall i, inc i z -> Vg f i <> \0c).
     set_extens v.
        move /(setIf_P _ nez) => p1.
        move: (p1 _ (rep_i nez)) => /Zo_P [p2 p3]; apply /Zo_P;split => //.
        by move => i iz; move: (p1 _ iz) => /Zo_P [_].
     move =>/Zo_P [p1 p2]; apply/(setIf_P _ nez) => j jz; apply /Zo_P;fprops.
  move: (sub_smaller zj); rewrite cJ - /k => kn.
  move: (BS_le_int kn hB) => kB.
  set Z := Zo _ _.
  pose ga f:= Lg J (fun i => Yo (inc i z) (cpred (Vg f i)) (Vg f i)).
  pose gb f:= Lg J (fun i => Yo (inc i z) (succ (Vg f i)) (Vg f i)).
  have pb : forall f, fgraph f -> allf f cardinalp -> domain f = J ->
       (forall i, inc i J -> inc (Vg f i) Bnat) ->
       (forall i, inc i z -> Vg f i <> \0c) ->
       card_sum (ga f) +c k = card_sum f.
    move => f p1 p2 p0 p3 p4.
    pose f2 := (graph (char_fun z J)).
    have q2: forall i, inc i J -> Vg (ga f) i +c Vg f2 i = Vg f i.
      move => i iJ; rewrite /ga /f2 -/(Vf _ i); bw; Ytac zi.
        rewrite (char_fun_V_a zj zi).
        move: (cpred_pr (p3 _ iJ) (p4 _ zi)) => [h1 h2].
        by rewrite -(Bsucc_rw h1) - h2.
      have aux: inc i (J -s z) by apply /setC_P.
      by rewrite char_fun_V_b //; aw; apply: p2; rewrite p0.
    set f3 := (Lg J (Vg f2)).
    have s1: fgraph f3 by rewrite /f3; by fprops.
    have s2: sub z (domain f3) by rewrite /f3; bw.
    have s3: forall i, inc i ((domain f3) -s z) -> Vg f3 i = \0c.
      rewrite /f3/f2; bw => i ij; bw; last by move /setC_P: ij => [].
      by rewrite -/(Vf _ _) (char_fun_V_b zj ij).
    have s4: Lg z (Vg f3) = cst_graph z \1c.
       apply : Lg_exten => i iz; move: (zj _ iz) => iJ; rewrite /f3; bw.
      exact (char_fun_V_a zj iz).
    move: (csum_zero_unit s2 s3); rewrite /card_sumb s4 csum_of_ones -/k => s5.
    move: (sum_of_sums (Vg (ga f)) (Vg f2) J); rewrite /card_sumb.
    have r1 : domain (ga f) = J by rewrite /ga; bw.
    have r3 : fgraph (ga f) by rewrite /ga; fprops.
    rewrite -{1} r1 (Lg_recovers r3) s5 => ->; apply: f_equal.
    apply: fgraph_exten; fprops; bw; first by symmetry.
    move => i ij /=; bw; exact (q2 _ ij).
  have pa: forall f, inc f Z ->
      [/\ k <=c n, inc (ga f) (Ak (n -c k)) & gb (ga f) = f].
    move => f /Zo_P [p0 p5].
    move /(setof_suml_auxP _ nB): (p0) => [p1 p2 p3 p4].
    have q1: forall i, inc i J -> inc (Vg f i) Bnat.
      move /funI_P: p0 => [f1] /Zo_P [] /fun_set_P [q0 q1 q2] q3 ->.
      rewrite - q1 => i isf; move: (Vf_target q0 isf); rewrite q2 => q4.
      exact (Bint_S q4).
    move: (pb _ p3 p4 p1 q1 p5) => q3.
    have r1 : domain (ga f) = J by rewrite /ga; bw.
    have q4: k <=c card_sum f.
      by rewrite - q3; rewrite csumC;apply:csum_M0le; fprops.
    have q5: k <=c n by apply: (card_leT q4 p2).
    move: (BS_diff k nB) =>q6.
    have q7: card_sum (ga f) <=c n -c k.
       have q4': card_sum (ga f) <=c card_sum f.
         by rewrite - q3; apply:csum_M0le; fprops.
       move: (BS_le_int (card_leT q4' p2) nB) => h1.
       move: p2; rewrite -q3 - {1} (cdiff_pr q5) csumC => s1.
       exact (csum_le_simplifiable kB h1 q6 s1).
    have r3 : fgraph (ga f) by rewrite /ga; fprops.
    have r4 : allf (ga f) cardinalp.
      red; rewrite /ga; bw => i ij; bw; move: (q1 _ ij) => ha; Ytac iz; fprops.
      move: (cpred_pr ha (p5 _ iz)) => [h1 h2]; fprops.
    have q8: inc (ga f) (Ak (n -c k)).
      apply (setof_suml_auxP _ q6); split => //; split => //.
    split => //; rewrite /gb;apply: fgraph_exten; [ fprops | done | by bw | bw].
    move => i iJ /=; bw; rewrite /ga; Ytac iz; bw; Ytac0; last by exact.
    by rewrite - (proj2 (cpred_pr (q1 _ iJ) (p5 _ iz))).
  case: (card_le_to_el (CS_Bnat kB) (CS_Bnat nB)) => aux; last first.
     have ->: Z = emptyset.
        apply /set0_P => t tz; move: (proj31 (pa _ tz)) => h1; co_tac.
     rewrite cardinal_set0 - (cdiff_pr kn); set i := h -c k.
     move: (BS_diff k hB) => iB.
     rewrite (csumC k) csumA (cdiff_pr1 (BS_sum nB iB) kB) (csumC i).
    by rewrite binom_bad //; fprops; apply: csum_Mlteq.
  have ->: (n +c h) -c k = (n -c k) +c h.
     rewrite -{1} (cdiff_pr aux) csumC (csumC k) (csumC _ h) csumA cdiff_pr1 //.
     fprops.
  move: (proj2 (set_of_functions_sum_pr (BS_diff k nB) hB)).
  rewrite (binom_symmetric2 (BS_diff k nB) hB) -/(Ak _) => <-.
  apply /card_eqP; exists (Lf ga Z (Ak (n -c k))); split;aw.
  move: (BS_diff k nB) =>q6.
  apply: lf_bijective.
      by move => f fa; move: (pa _ fa)=> [_ ok _].
   move => u v uz vz sw; move: (pa _ uz) (pa _ vz) => [_ _ e1][_ _ e2].
   by rewrite - e1 -e2 sw.
   move =>y yf.
    move /(setof_suml_auxP _ q6): (yf) => [p1 p2 p3 p4].
    have q1: forall i : Set, inc i J -> inc (Vg y i) Bnat.
      move /funI_P: yf => [f1] /Zo_P [] /fun_set_P [q0 q1 q2] q3 ->.
      rewrite - q1 => i isf; move: (Vf_target q0 isf); rewrite q2 => q4.
      exact (Bint_S q4).
    have q5:forall i, inc i z -> Vg (gb y)i <> \0c.
      move => i iz; move: (zj _ iz) => iJ;rewrite /gb; bw; Ytac0.
      apply: succ_nz.
    have q4: ga (gb y) = y.
      move: yf; rewrite /Ak; move /(setof_suml_auxP J q6)=> [s1 s2 s3 s4].
      rewrite /ga; apply: fgraph_exten; fprops; bw => //.
      move => i iJ /=; bw; rewrite /gb; bw; Ytac zi; Ytac0; last by exact.
      by apply: cpred_pr2; apply: q1.
    have q2: fgraph (gb y) by rewrite /gb; fprops.
    have dgb: (domain (gb y)) = J by rewrite /gb; bw.
    have q7: forall i, inc i J -> inc (Vg (gb y) i) Bnat.
      move => i ij; move: (q1 _ ij) => ha;rewrite /gb; bw; Ytac zi; fprops.
    have q3: (allf (gb y) cardinalp).
      move => i; rewrite dgb => ij; rewrite /gb; bw; Ytac zi; fprops.
  exists (gb y) => //.
  apply /Zo_P;split => //; apply /(setof_suml_auxP _ nB) => //;split => //.
    move: (pb _ q2 q3 dgb q7 q5); rewrite q4; move => <-.
    rewrite - (cdiff_pr aux) csumC; apply: csum_Mlele => //; fprops.
move: (Exercise5_5_b3 Bk fsj).
set s1 := card_sumb _ _;set s2 := card_sumb _ _.
set s3 := card_sumb _ _; set s4 := card_sumb _ _.
set fct0:= cst_graph J \0c.
have fct0_ok: inc fct0 (Ak n).
   apply /setof_suml_auxP => //; rewrite /fct0; bw;split => //.
      rewrite csum_of_same; aw; rewrite cprodC cprod0r; fprops.
     fprops.
   hnf; bw; move => t tj; bw; fprops.
have ue: (unionf J Bk) = Ak n -s1 fct0.
   set_extens t.
     move => /setUf_P [z tz] /Zo_P [ta tb].
     apply /setC1_P; split => //; dneg eq2; rewrite eq2 /fct0; bw.
   move => /setC1_P [t1 t2]; apply /setUf_P.
   move /(setof_suml_auxP _ nB): (t1) => [t4 _ t5 t6].
   suff: (exists2 i, inc i J & Vg t i <> \0c).
     move => [i ij t3]; ex_tac; apply /Zo_P;split => //.
   ex_middle bad; case: t2; rewrite /fct0.
   apply: fgraph_exten => //; bw; fprops.
   rewrite t4; move => s st /=; bw; ex_middle ok; case: bad; ex_tac.
suff [ -> ->]: s1 = s3 /\ s2 = s4.
  have cb1: cardinalp (binom (n +c h) h) by apply: CS_Bnat; apply:BS_binom.
  move: (card_succ_pr2 fct0_ok); rewrite -ue card_succ_pr4; last by fprops.
  rewrite csumC (cprod1l cb1) (binom_symmetric2 nB hB).
  rewrite (proj2 (set_of_functions_sum_pr nB hB)) => -> <-.
  by rewrite csumC - csumA.
split.
   have ->: s1 = card_sumb (even_card0_sub J)
        (fun z => binom ((n +c h) -c (cardinal z)) h).
     rewrite /s1/card_sumb; apply: f_equal; apply: Lg_exten => t.
     move => /Zo_P [] /Zo_P [] /setP_P ta tb /set1_P tc; apply: r1 => //.
     by apply /nonemptyP.
   set X := (even_card0_sub J); set F := (A -s1 \0c).
   have pa: (forall x : Set, inc x X -> inc (cardinal x) F).
      move => x /Zo_P [] /Zo_P [] /setP_P wJ pa /set1_P pb; apply /Zo_P; split.
         apply /Zo_P;split => //;apply /(BintcP hB).
         rewrite - cJ; apply:(sub_smaller wJ).
         move /set1_P=> ha; case: pb; exact: (cardinal_nonemptyset ha).
   rewrite (card_partition_induced1 _ pa).
   rewrite /s3 /card_sumb; apply: f_equal; apply: Lg_exten => i iF.
   rewrite /f'; set Y:= Zo _ _.
   transitivity (card_sum (cst_graph Y (binom ((n +c h) -c i) h))).
     rewrite /cst_graph; apply: f_equal; apply: fgraph_exten; fprops; bw.
     by move => j jY /=;bw; move /Zo_P: jY => [_ ->].
   rewrite csum_of_same cprodC; apply: cprod2_pr2 => //.
   move /Zo_P: iF => [] /Zo_P [i1 i2] /set1_P i3; move: (Bint_S i1) => i4.
   have ->: Y = subsets_with_p_elements i J.
     set_extens t.
       by move => /Zo_P [] /Zo_P [] /Zo_P [t1 t2] t3 t4; apply /Zo_P.
    move => /Zo_P [t1 t2]; apply/Zo_P;split => //; apply /Zo_P;split => //.
      by apply /Zo_P;split => //; rewrite t2.
    by move => /set1_P => te; case: i3; rewrite - t2 te cardinal_set0.
    rewrite - (subsets_with_p_elements_pr hB i4 cJ).
    by rewrite card_card //; apply: CS_Bnat; apply: BS_binom.
have ->: s2 = card_sumb (odd_card_sub J)
        (fun z => binom ((n +c h) -c (cardinal z)) h).
  rewrite /s2/card_sumb; apply: f_equal; apply: Lg_exten => t.
  move => /Zo_P [] /setP_P ta tb; apply: r1 => //.
  by apply: odd_nonempty.
set X := (odd_card_sub J); set F := (Zo I odd_int).
have pa: (forall x : Set, inc x X -> inc (cardinal x) F).
  move => x /Zo_P [] /setP_P pa pb; apply /Zo_P;split => //.
  apply /(BintcP hB); rewrite - cJ; apply:(sub_smaller pa).
rewrite (card_partition_induced1 _ pa).
rewrite /s4 /card_sumb; apply: f_equal; apply: Lg_exten => i iF.
rewrite /f'; set Y:= Zo _ _.
transitivity (card_sum (cst_graph Y (binom ((n +c h) -c i) h))).
   rewrite /cst_graph; apply: f_equal; apply: fgraph_exten; fprops; bw.
    by move => j jY /=;bw; move /Zo_P: jY => [_ ->].
rewrite csum_of_same cprodC; apply: cprod2_pr2 => //.
move /Zo_P: iF => [i1 i2]; move: (Bint_S i1) => i3.
have ->: Y = subsets_with_p_elements i J.
    set_extens t.
       move => /Zo_P [] /Zo_P [t1 t2] t3; apply /Zo_P;split => //.
   move => /Zo_P [t1 t2]; apply/Zo_P;split => //.
   by apply /Zo_P;split => //; rewrite t2.
rewrite - (subsets_with_p_elements_pr hB i3 cJ).
by rewrite card_card //; apply: CS_Bnat; apply: BS_binom.
Qed.


Definition surjections E F :=
  Zo (functions E F)(surjection).

Definition nbsurj n p :=
   cardinal(surjections (Bint n) (Bint p)).

Lemma nbsurj_pr E F:
  finite_set E -> finite_set F ->
  cardinal (surjections E F) = nbsurj (cardinal E) (cardinal F).
Proof.
move => pa pb.
set n := (cardinal E); set m := (cardinal F).
have nB: inc n Bnat by apply /BnatP.
have mB: inc m Bnat by apply /BnatP.
move: (card_Bint nB)(card_Bint mB).
move/card_eqP => [g [fg sg tg]].
move/card_eqP => [h [fh sh th]].
apply/card_eqP.
set s:= (surjections E F).
set t := surjections _ _.
move: (inverse_bij_fb fh) => bih.
set j := (fun f => (inverse_fun h) \co f \co g).
have pc: forall f, inc f s ->
  (inverse_fun h \coP f)/\ (inverse_fun h \co f) \coP g.
  move => f /Zo_P [] /fun_set_P [ff sf tf] sjf.
  have s1: inverse_fun h \coP f by split => //; aw; try fct_tac; ue.
  split => //; split => //; aw; try ue; try fct_tac.
exists (Lf (fun f => (inverse_fun h) \co f \co g) s t).
split;aw;apply: lf_bijective.
    move => f fp; move: (pc _ fp)=> [s1 s2]; apply/ Zo_P;split => //.
      apply /fun_set_P;red;aw;split => //; fct_tac.
      move/ Zo_hi: fp => sjf.
    move: (compose_fs sjf (proj2 bih) s1) => s3; apply:compose_fs => //.
    exact (proj2 fg).
  move => u v us vs; move: (pc _ us) (pc _ vs)=> [s1 s2][s3 s4] s5.
  move: (compf_regl fg s2 s4 s5) => s6.
  by move: (compf_regr bih s1 s3 s6).
move => y /Zo_P []/fun_set_P [fy sy ty] sjy.
set f := (h \co (y \co inverse_fun g)).
move: (inverse_bij_fb fg) => big.
have s1: (y \coP inverse_fun g) by split => //;aw; try fct_tac; ue.
have s2: h \coP (y \co inverse_fun g) by split => //; aw; try ue; try fct_tac.
have fs: inc f s.
  apply/ Zo_P; split.
    by rewrite /f;apply /fun_set_P;split => //; aw;try fct_tac.
  move: (compose_fs (proj2 big) sjy s1) => s3; apply:compose_fs => //.
  exact (proj2 fh).
exists f => //; rewrite /f (compfA (composable_inv_f fh) s2).
have pd: (source h) = target (y \co inverse_fun g) by aw; ue.
  rewrite (bij_left_inverse fh) pd (compf_id_l (proj32 s2)).
rewrite - (compfA s1 (composable_inv_f fg)) (bij_left_inverse fg) sg - sy.
by symmetry;apply (compf_id_r).
Qed.

Lemma nbsurj_rec n p: inc n Bnat -> inc p Bnat ->
  nbsurj (succ n)(succ p) =
   (succ p) *c ( nbsurj n p +c nbsurj n (succ p)).
Proof.
move => nB pB; rewrite {1} /nbsurj csumC.
move: (BS_succ pB) => spB.
set I := (Bint (succ n)); set J:= (Bint (succ p)).
set I' := Bint n.
set E := (surjections I J).
pose phi := Lf (fun f => Vf f n) E J.
have sphi: E = source phi by rewrite /phi; aw.
have pa: succ p = cardinal (target phi).
  by rewrite /phi; aw; rewrite (card_Bint spB).
rewrite {1} pa sphi; clear pa.
have lfa: lf_axiom (Vf ^~n) E J.
  move => f /Zo_P [] /fun_set_P [pa pb pc] _.
  by Wtac; rewrite pb; apply:Bint_si.
have fphi: function phi by apply: lf_function.
apply:(shepherd_principle fphi).
rewrite {1} /phi; aw; move => x xJ.
set F := inv_image_by_fun phi (singleton x).
have fp: forall f, inc f F <-> inc f (surjections I J) /\ x = Vf f n.
  move => f; split.
    move /(iim_fun_set1_P _ fphi) => []; rewrite - sphi => fe;rewrite{1}/phi.
    by aw; move => pa.
  move => [pa pb]; apply /(iim_fun_set1_P _ fphi).
  split => //;[ ue | rewrite /phi;aw].
pose sfx f := exists2 y, inc y I' & Vf f y = x.
have ii': sub I' I by apply: Bint_M.
set A1 := Zo F sfx.
have <-: cardinal A1 = nbsurj n (succ p).
  apply /card_eqP.
  exists (Lf (restriction^~ I' ) A1 (surjections I' J)); split;aw.
  apply /lf_bijective.
      move => f /Zo_P [] /fp [] /Zo_P [] /fun_set_P [ff sf tf] sjf fn sff.
      have si: sub I' (source f) by rewrite sf.
      move: (restriction_prop ff si); rewrite tf => fp'.
      apply /Zo_P; split; first by apply /fun_set_P.
      move: fp' => [sa sb sc]; split; first by exact.
      rewrite sc sb - tf=> y ytf; move: (proj2 sjf _ ytf) => [a asf va].
      move: asf; rewrite sf; move /(BintsP nB) => lean.
      case: (equal_or_not a n) => lan.
        move: sff => [b ba bb]; rewrite - va lan - fn - bb; ex_tac.
        rewrite restriction_V //.
      have aI: inc a I' by apply /(BintP nB).
      by exists a => //; rewrite restriction_V.
    move => f g /Zo_P [] /fp [] /Zo_P [] /fun_set_P [ff sf tf] sjf fn sff.
    move => /Zo_P [] /fp [] /Zo_P [] /fun_set_P [fg sg tg] sjg gn sfg sr.
    apply: function_exten => //; (try ue); move => i isf /=.
    move: isf; rewrite sf; move /(BintsP nB) => lein.
    case: (equal_or_not i n) => lin; first by rewrite lin - fn gn.
    have iI: inc i I' by apply /(BintP nB); split.
    have si: sub I' (source f) by rewrite sf.
    have sj: sub I' (source g) by rewrite sg - sf.
    move: (f_equal (Vf^~ i) sr); rewrite restriction_V // restriction_V //.
  move => y /Zo_P [] /fun_set_P [fy sy ty] sjy.
  move: (Bint_pr4 nB); rewrite -/I -/I' - sy; move => [ci pa].
  move:(extension_fs x fy pa sjy) => sjf.
  have pb: sub I' (source (extension y n x)).
       by rewrite /extension sy; aw; fprops.
  move:(proj1 sjf) => fjf.
  have si: source (extension y n x) = I by rewrite /extension; aw.
  have ti: target (extension y n x) = J.
    rewrite /extension ty; aw; rewrite setU1_eq //.
  have fx: Vf (extension y n x) n = x by rewrite extension_Vf_out.
  have re : (restriction (extension y n x) I') = y.
  move: (restriction_prop fjf pb) => [pc pd pe].
  apply : function_exten => //; rewrite ? pd ?pe ? ti//.
  move => i ii /=;rewrite restriction_V //.
    by rewrite extension_Vf_in // sy.
  have aux: sfx (extension y n x).
     rewrite -ty in xJ; move: (proj2 sjy _ xJ) => [s sa sb].
     exists s; [ ue | rewrite extension_Vf_in //].
   exists (extension y n x);last by ue.
  by apply:Zo_i=> //;apply /fp; split => //; apply:Zo_i=> //; apply /fun_set_P.
have sa1: sub A1 F by apply: Zo_S.
rewrite (cardinal_setC2 sa1) csum2_pr2a - csum2_pr2b; congr (_ +c _).
have pa: n = cardinal I' by rewrite (card_Bint nB).
have fs1: finite_set I' by red; rewrite -pa;apply /BnatP.
have pb: p = cardinal (J -s1 x).
  move: (card_succ_pr2 xJ); rewrite (card_Bint spB) => h.
  apply: succ_injective1 => //; fprops.
have fs2: finite_set (J -s1 x) by red; rewrite -pb;apply /BnatP.
rewrite pa pb - (nbsurj_pr fs1 fs2).
apply /card_eqP.
have pc: forall f, inc f (F -s A1) -> restriction2_axioms f I' (J -s1 x).
  move => f /setC_P [fF fp1].
  move: (fF) => /fp [] /Zo_P[] /fun_set_P [ff sf tf] sjf fn.
  have aux: sub I' (source f) by ue.
  red; rewrite sf tf; split => //; try apply: sub_setC.
  move => i /(Vf_image_P ff aux) [u ui ->]; apply /setC1_P; split.
      rewrite -tf; Wtac.
  by dneg fa1; apply /Zo_P;split => //; exists u.
exists (Lf (fun z => restriction2 z I' (J -s1 x))
  (F -s A1) (surjections I' (J -s1 x))); split;aw.
apply /lf_bijective.
    move => f fa /=; move: (pc _ fa) => a1.
    move: (restriction2_prop a1) => a2.
    move: fa => /Zo_P [] /fp [] /Zo_P [] /fun_set_P [ff sf tf] sjf fn sff.
    apply /Zo_P;split; first by apply /fun_set_P.
    move: a2 => [a3 a4 a5]; split; first by exact.
    rewrite a4 a5 - {1} tf=> y /setC1_P [ytf xx].
    move: (proj2 sjf _ ytf) => [a asf va].
    move: asf; rewrite sf; move /(BintsP nB) => lean.
    case: (equal_or_not a n) => lan; first by case: xx; rewrite fn - va lan.
    have aI: inc a I' by apply /(BintP nB); split.
    by exists a => //; rewrite restriction2_V.
  move => f g fa fb sr.
  move: (pc _ fa) (pc _ fb) => a1 a2.
  move: fa => /setC_P [] /fp [] /Zo_P [] /fun_set_P [ff sf tf] _ fv _.
  move: fb => /setC_P [] /fp [] /Zo_P [] /fun_set_P [fg sg tg] _ gv _.
  apply: function_exten => //; (try ue); move => i isf /=.
  move: isf; rewrite sf; move /(BintsP nB) => lein.
  case: (equal_or_not i n) => lin; first by rewrite lin - fv gv.
  have iI: inc i I' by apply /(BintP nB); split.
  move: (f_equal (Vf^~ i) sr); rewrite restriction2_V // restriction2_V //.
move => y /Zo_P [] /fun_set_P [fy sy ty] sjy.
move: (Bint_pr4 nB); rewrite -/I -/I' - sy; move => [ci pd].
move:(extension_fs x fy pd sjy) => sjf.
have pe: sub I' (source (extension y n x)).
  by rewrite /extension sy; aw; fprops.
move:(proj1 sjf) => fjf.
have si: source (extension y n x) = I by rewrite /extension; aw.
have ti: target (extension y n x) = J.
by rewrite /extension ty; aw; apply:setC1_K.
have fx: Vf (extension y n x) n = x by rewrite extension_Vf_out.
move: (extension_restr x fy pd); rewrite ty => pf.
exists (extension y n x) => //; apply/setC_P; split.
  by apply /fp; split => //; apply /Zo_P; split => //; apply /fun_set_P.
  move /Zo_P => [sa [z]]; rewrite - sy => sb;rewrite extension_Vf_in // => pg.
  by move: (Vf_target fy sb); rewrite pg ty => /setC1_P [].
Qed.

Definition partitionsx E p :=
  Zo (powerset (powerset E)) (fun z => partition_s z E /\ cardinal z = p).

Definition nbpart n p :=
  cardinal(partitionsx (Bint n) p).

Lemma nbpart_pr1 E F g p
    (f := fun_image ^~ (image_by_fun g)):
    bijection g -> source g = E -> target g = F ->
    bijection (Lf f (partitionsx E p)(partitionsx F p)).
Proof.
rewrite /f; clear f; move: E F g.
have aux: forall E F g (f := fun_image ^~ (image_by_fun g))
     (f' := fun_image ^~ (image_by_fun (inverse_fun g))),
     bijection g -> source g = E -> target g = F ->
    forall x, inc x (partitionsx E p) -> f' (f x) = x.
  move => E F g f f' bg sg tg x.
  move => /Zo_P [pa [pb pc]]; rewrite /f/f'.
  have aux: forall t, inc t x -> sub t (source g).
    by move => t tx; rewrite sg; apply /setP_P; move /setP_P: pa; apply.
  set_extens t.
    move /funI_P => [z] /funI_P [w wx ->].
    by rewrite - (inverse_direct_image_inj (proj1 bg) (aux _ wx)); move ->.
  move => tx; apply /funI_P.
  rewrite (inverse_direct_image_inj (proj1 bg) (aux _ tx));
  exists (image_by_fun g t) => //; apply /funI_P; ex_tac.
have aux2: forall E F g (f := fun_image ^~ (image_by_fun g)),
    bijection g -> source g = E -> target g = F ->
    lf_axiom f (partitionsx E p)(partitionsx F p).
  move => E F g f big sg tg; move: (proj1 (proj1 big)) => fg.
  rewrite /f;move => pr /Zo_P [p1 [p2 p3]].
  move: p2 => [[p4 p6] p5].
  set K:= (fun_image pr (image_by_fun g)).
  have ax: forall z, inc z pr -> sub z (source g).
    move => z zpr; move: p1 => /setP_P sa; move: (sa _ zpr) => /setP_P; ue.
  have pr1: inc K (powerset (powerset F)).
    apply /setP_P => t; move /funI_P => [z zpr ->]; apply /setP_P => s.
    move: (ax _ zpr) => a1.
    move /(Vf_image_P fg a1) => [u uz ->]; rewrite -tg; Wtac.
  have pr2: union K = F.
    rewrite -tg;set_extens s.
      move /setU_P=> [a sa] /funI_P [z zpr e1];move: (ax _ zpr) => a1.
      move: sa; rewrite e1; move /(Vf_image_P fg a1) => [u uz ->]; Wtac.
    move => si; move: (bij_surj big si); rewrite sg -p4; move => [x].
    move/setU_P => [z xz] zpr <-; apply /setU_P;exists (image_by_fun g z).
       by apply (Vf_image_P fg (ax _ zpr)); ex_tac.
    apply /funI_P; ex_tac.
  have pr3: alls K nonempty.
    move => t /funI_P [z zpr ->]; move: (p5 _ zpr) => [a az].
    exists (Vf g a); apply /(Vf_image_P fg (ax _ zpr)); ex_tac.
  have pr4: partition_s K F.
    split => //; split => //; move => a b ak bk; mdi_tac nab.
    move: ak bk nab => /funI_P [a1 a1p ->] /funI_P [b1 b1p ->].
    move:(ax _ a1p)(ax _ b1p) => s1 s2.
    case: (p6 _ _ a1p b1p); [ by move => -> | move => diab _ ].
    move => u /(Vf_image_P fg s1) [a2 a2p ->].
    move /(Vf_image_P fg s2)=> [b2 b2p b2v].
    move: (bij_inj big (s1 _ a2p) (s2 _ b2p)b2v) => sb.
    empty_tac1 a2; ue.
  apply /Zo_P;split => //; split => //.
  rewrite -p3; symmetry; apply /card_eqP.
  exists (Lf (fun z => (image_by_fun g z)) pr K); split;aw.
  have ifi: forall s1 s2, sub s1 (source g) -> sub s2 (source g) ->
     image_by_fun g s1 = image_by_fun g s2 -> s1 = s2.
    move => s1 s2 aa bb cc.
    rewrite (inverse_direct_image_inj (proj1 big) aa).
    by rewrite (inverse_direct_image_inj (proj1 big) bb) cc.
  apply: lf_bijective.
      move => z zp; apply /funI_P; ex_tac.
    move => u v ui vi si; exact: (ifi _ _ (ax _ ui) (ax _ vi) si).
  move => y yK.
  have aux2: sub y (target g) by rewrite tg - pr2; apply: setU_s1.
  move: (direct_inv_im_surjective (proj2 big) aux2).
  set s := (image_by_fun (inverse_fun g) y) => hh; exists s => //.
  move: (inverse_bij_fb big) => [[fib _] _].
  have syis: sub y (source (inverse_fun g)) by aw.
  have ssg: sub s (source g).
    have ->: (source g) = target (inverse_fun g) by aw.
    move => t /(Vf_image_P fib syis) [u uy ->]; Wtac.
  move: yK => /funI_P [w wp]; rewrite -hh => h1.
  by rewrite (ifi _ _ ssg (ax _ wp) h1).
move => E F g pa pb pc.
set f := (fun_image^~ (image_by_fun g)).
pose g' := inverse_fun g.
move: (inverse_bij_fb pa) => pa'.
have pb': source g' = F by rewrite /g'; aw.
have pc': target g' = E by rewrite /g'; aw.
move: (aux2 _ _ _ pa pb pc) => h.
move: (aux2 _ _ _ pa' pb' pc').
set f' := fun_image^~ (image_by_fun g') => h'.
have ff': forall x, inc x (partitionsx E p) -> f' (f x) = x.
   by move => x; apply: aux.
apply: lf_bijective => //.
  by move => u v uK vK sf; rewrite - (ff' _ uK) - (ff' _ vK) sf.
move => y yp.
move: (h' _ yp) => u1; move: (ff' _ u1) => u2.
exists (f' y) => //.
have ->: f = fun_image^~ (image_by_fun (inverse_fun g')).
     rewrite /g' ifun_involutive //; fct_tac.
by symmetry; apply: aux => //; rewrite /g'; aw; rewrite pc.
Qed.

Lemma nbpart_pr E p:
  finite_set E -> cardinal (partitionsx E p) = nbpart (cardinal E) p.
Proof.
move => fse; set n := (cardinal E).
have nB: inc n Bnat by apply /BnatP.
have : n = cardinal (Bint n) by rewrite (card_Bint nB).
move/card_eqP => [g [big sg tg]].
move: (nbpart_pr1 p big sg tg); set f := Lf _ _ _ => bf.
apply /card_eqP; exists f; rewrite /f; split; aw.
Qed.

Lemma nbsurj_part n p: inc n Bnat -> inc p Bnat ->
  nbsurj n p = (factorial p) *c (nbpart n p).
Proof.
move => nB pB.
rewrite /nbsurj /nbpart.
set I := (Bint n); set J:= (Bint p).
have cj: p = cardinal J by rewrite (card_Bint pB).
set E := (surjections I J).
set K := (partitionsx I p).
pose f g := fun_image J (fun z => inv_image_by_fun g (singleton z)).
have lfa: lf_axiom f E K.
  move => g /Zo_P [] /fun_set_P [fg sg tg] sjg.
  have p1: inc (f g) (powerset (powerset I)).
     apply /setP_P => z /funI_P [w wJ ->]; apply /setP_P => t.
     by move /(iim_fun_set1_P w fg) => []; rewrite sg.
  have p2: cardinal (f g) = p.
    symmetry; rewrite cj; apply /card_eqP.
    exists (Lf (fun z => inv_image_by_fun g (singleton z)) J (f g)).
    split;aw; apply lf_bijective.
        move => z zj; apply /funI_P; ex_tac.
      move => u v uj vj si.
      rewrite -tg in uj; move: (proj2 sjg _ uj) => [x xsg h].
      symmetry in h;move: (iim_fun_set1_i fg xsg h); rewrite si => xi.
      by rewrite (iim_fun_set1_hi fg xi) - h.
    by move => y /funI_P.
  have p3: union (f g) = I.
    set_extens t.
      move =>/setU_P [z tz h]; move /setP_P: p1 => h1.
      by move: (h1 _ h) => /setP_P; apply.
    move => ti; apply /setU_P; exists (inv_image_by_fun g (singleton (Vf g t))).
    rewrite - sg in ti.
       by exact: (iim_fun_set1_i fg ti (refl_equal (Vf g t))).
    apply /funI_P; exists (Vf g t) => //; rewrite -tg; Wtac.
  have p4: alls (f g) nonempty.
     move => z /funI_P [t]; rewrite - tg => ttg ->.
     move: (proj2 sjg _ ttg) => [x xsg h].
     symmetry in h; move: (iim_fun_set1_i fg xsg h) => h1; ex_tac.
  apply /Zo_P;split => //; split => //; split => //; split => //.
  move => a b a1 b1; mdi_tac nab => u ua ub; case: nab; move: ua ub.
  move /funI_P: a1 => [z zj ->]; move /funI_P: b1 => [w wj ->].
  by move => h1 h2;rewrite (iim_fun_set1_hi fg h1) - (iim_fun_set1_hi fg h2).
pose phi := Lf f E K.
have sphi: E = source phi by rewrite /phi; aw.
have ->: K = target phi by rewrite /phi; aw.
have fphi: function phi by apply: lf_function.
rewrite sphi cprodC; apply: (shepherd_principle fphi).
rewrite {1} /phi; aw; move => x xK.
set F := inv_image_by_fun phi (singleton x).
have fp: forall g, inc g F <-> inc g (surjections I J) /\ f g = x.
  move => g; split.
    move /(iim_fun_set1_P _ fphi) => []; rewrite - sphi => fe;rewrite{1}/phi.
    aw; move => pa;split => //.
  move => [pa pb]; apply /(iim_fun_set1_P _ fphi).
  by split => //;[ ue | rewrite /phi;aw].
move: (xK) => /Zo_P [xpp [px]]; rewrite cj.
move /card_eqP => [fa [bfa sfa tfa]].
pose fb t := select (fun s => inc t s) x.
have prb: forall t, inc t I -> inc t (fb t) /\ inc (fb t) x.
  move => t ti; apply: (select_pr); move: px => [[pa pc] pb].
    move: ti; rewrite - pa => /setU_P [z za zb]; ex_tac.
  move => a b sa sb sc sd; case: (pc _ _ sa sc) => // h; empty_tac1 t.
pose fc := Lf (fun t => (Vf fa (fb t))) I J.
have sfc: source fc = I by rewrite /fc; aw.
have tfc: target fc = J by rewrite /fc; aw.
have fc0: lf_axiom (fun t => (Vf fa (fb t))) I J.
   move=> t ti; move: (prb _ ti) => [_]; rewrite - sfa - tfa => h; Wtac;fct_tac.
have fc1: function fc by apply: lf_function.
have fc2': surjection fc.
  split => // y; rewrite /fc; aw; rewrite - tfa => yJ.
  move: (bij_surj bfa yJ); rewrite sfa; move => [z zx <-].
  move: px => [[p1 p3 p2]]; move: (p2 _ zx) => [t tz].
  have ti: inc t I by rewrite - p1; union_tac.
  rewrite tfa;ex_tac; aw.
  move: (prb _ ti) => [sa sb]; case: (p3 _ _ zx sb); first by move => ->.
  move => h; empty_tac1 t.
have fc2: inc fc (surjections I J).
  apply /Zo_P; split => //; by apply /fun_set_P.
have fc3: forall w, inc w x -> inv_image_by_fun fc (singleton (Vf fa w)) = w.
  move => w wx; move: px => [[p1 p3] p2]; set_extens s.
    move /(iim_fun_set1_P _ fc1); rewrite sfc /fc; move => [ta]; aw.
    move => vfa; move: (prb _ ta) => [tb tc].
    by rewrite - sfa in wx tc; rewrite (bij_inj bfa wx tc vfa).
  move => sw; apply /(iim_fun_set1_P _ fc1).
  have si: inc s I by rewrite - p1; union_tac.
  rewrite sfc /fc;aw;split => //; move: (prb _ si) => [tb tc].
  case: (p3 _ _ wx tc); [by move => <- | by move =>h; empty_tac1 s].
have fc4: inc fc F.
  move: (proj1 (proj1 bfa)) => ffa.
  apply /fp; split => //; rewrite /f;set_extens t.
    move /funI_P => [z zJ ->]; rewrite -tfa in zJ.
    move: (bij_surj bfa zJ); rewrite sfa; move => [w wx <-].
    by rewrite (fc3 _ wx).
  move => tx; apply /funI_P; exists (Vf fa t); first by Wtac.
  by rewrite (fc3 _ tx).
have fsj: finite_set J by red; rewrite - cj; apply /BnatP.
rewrite - (number_of_permutations fsj).
symmetry; clear fsj; apply /card_eqP.
exists (Lf (fun z => z \co fc) (permutations J) F); split; aw.
move /Zo_P: (fc2) => [sa sb]; move: (exists_right_inv_from_surj sb) => [s sc].
apply /lf_bijective.
    move => g /Zo_P [] /fun_set_P [fg sg tg] big.
    have gfc: g \coP fc by split => //; rewrite sg tfc.
    have fgfc: function (g \co fc) by fct_tac.
    have tgfc: target (g \co fc) = J by aw.
    have sgfc: source (g \co fc) = I by aw.
    have ssgfc: surjection(g \co fc) by apply/compose_fs =>//;exact (proj2 big).
    have pa:inc (g \co fc) (surjections I J).
     apply /Zo_P; split; first by apply/fun_set_P;aw.
     by apply /compose_fs => //; exact (proj2 big).
    have aux2: forall w, inc w I ->
      (inv_image_by_fun (g \co fc) (singleton (Vf (g \co fc) w)))=
      (inv_image_by_fun fc (singleton (Vf fc w))).
      move => w wi; set_extens t.
        move /(iim_fun_set1_P _ fgfc); rewrite sgfc; move => [tI].
        rewrite - sfc in wi tI;aw.
        move: (Vf_target fc1 wi) (Vf_target fc1 tI); rewrite tfc - sg.
        move => i1 i2 i3; rewrite (bij_inj big i1 i2 i3).
        by apply: (iim_fun_set1_i fc1 tI).
      rewrite - sfc in wi; move /(iim_fun_set1_P _ fc1) => [ta tb]; aw.
      apply:(iim_fun_set1_i fgfc); aw; ue.
    move /fp: fc4 => [_] xv1.
    apply /fp;split => //; set_extens t.
      move /funI_P => [z zJ ->].
      rewrite -tgfc in zJ; move: (proj2 ssgfc _ zJ); rewrite sgfc.
      move => [a ai <-]; rewrite (aux2 _ ai) - xv1.
      apply /funI_P;exists (Vf fc a) => //; Wtac.
    rewrite -xv1; move /funI_P => [z zj etc].
    apply /funI_P; rewrite -tfc in zj; move: (proj2 fc2' _ zj) etc.
    move => [a]; rewrite sfc => s1 <-; rewrite - (aux2 _ s1) => ->.
    exists (Vf (g \co fc) a) => //; rewrite - tgfc; Wtac.
  move => u v up vp sv; move: sc => [sc sd].
  move: up vp sa => /Zo_P [] /fun_set_P [fu su tu] _ /Zo_P [] /fun_set_P.
  move => [fv srv tv] _ /fun_set_P [fs sss ts].
  have c1: u \coP fc by split => //; ue.
  have c2: v \coP fc by split => //; ue.
  move: (f_equal (fun z => z \co s) sv).
  by rewrite - !compfA // sd ts - {1} su (compf_id_r fu) - srv (compf_id_r fv).
move => y yf.
move /fp: yf => [] /Zo_P []/fun_set_P [fy sy ty] sjy fyv.
move /Zo_P: fc2 => [_ sj1].
have sysj: source y = source fc by ue.
have aux: forall x0 y0 : Set,
   inc x0 (source fc) ->
   inc y0 (source fc) -> Vf fc x0 = Vf fc y0 -> Vf y x0 = Vf y y0.
   rewrite sfc; move => a b aI bI; rewrite /fc; aw => sv.
   move: (prb _ aI)(prb _ bI) => [s1 s2] [s3 s4].
   rewrite - sfa in s2 s4; move: (bij_inj bfa s2 s4 sv) => sf.
   move: s2; rewrite sfa - fyv; move /funI_P => [z zj] => ta.
   move: s1; rewrite ta => s1; rewrite - (iim_fun_set1_hi fy s1).
   by move: s3; rewrite - sf ta => s2; rewrite (iim_fun_set1_hi fy s2).
set h:= y \co s.
have pr1: fc \coP s by move:sc => [s1 s2].
have pr2: y \coP s by red;move: pr1 => [s1 s2 <-].
move:(sc) => [[_ s2 s3] s4].
have fh: function h by rewrite /h; fct_tac => //; rewrite sy - s3 sfc.
move: (f_equal source s4); aw; rewrite tfc => srs.
have hf: inc h (functions J J).
   by apply /fun_set_P; red; rewrite {2 3} /h; aw.
have sjh: surjection h.
  split => // y1; rewrite /h; aw => y1y; move: (proj2 sjy _ y1y).
  rewrite sy srs; move => [a ai <-].
  set b := Vf fc a; have bj: inc b J by rewrite - tfc /b; Wtac.
  have bs: inc b (source s) by ue.
  have bs3: inc (Vf s b) I by rewrite - sfc s3; Wtac.
  ex_tac; aw; apply: aux; rewrite ? sfc //.
  move: (f_equal (Vf^~ b) s4); aw; rewrite identity_V //; ue.
have bh: bijection h.
   move /fun_set_P: hf => [_ sh th].
   apply: bijective_if_same_finite_c_surj; rewrite ? sh ? th=> //.
   by red; rewrite - cj; apply /BnatP.
rewrite -(left_composable_value fy sj1 sysj aux sc (refl_equal h)).
by exists h=> //;apply /Zo_P.
Qed.

Lemma nbsurj_inv n p: inc n Bnat -> inc p Bnat ->
 p ^c n = card_sumb (Bintc p)
     (fun k => (binom p k) *c (nbsurj n k)).
Proof.
move => nB pB.
set I := (Bint n); set J:= (Bint p).
have ci: n = cardinal I by rewrite (card_Bint nB).
have cj: p = cardinal J by rewrite (card_Bint pB).
set K := (Bintc p).
have ->: p ^c n = cardinal (functions I J).
   rewrite ci cj; apply:cpow_pr; fprops.
have pa: forall x, inc x (functions I J) -> sub (image_of_fun x) J.
  by move => x /fun_set_P [p1 p2 <-]; apply:fun_image_Starget.
have pb: forall x, inc x (functions I J) ->
   inc (cardinal (image_of_fun x)) K.
   move => x h; move: (sub_smaller (pa _ h)).
   by rewrite - cj; move /(BintcP pB).
rewrite (card_partition_induced pb); rewrite /card_sumb; apply:f_equal.
apply: Lg_exten => k; move/(BintcP pB) => kp.
move: (BS_le_int kp pB) => kB.
rewrite (subsets_with_p_elements_pr pB kB (sym_eq cj)).
set E1 := Zo _ _; set K1 := subsets_with_p_elements _ _.
have pc: forall c, inc c E1 -> inc (image_of_fun c) K1.
  by move => c /Zo_P [pc pd]; apply /Zo_P;split => //; apply /setP_P; apply: pa.
pose phi := Lf image_of_fun E1 K1.
have sphi: E1 = source phi by rewrite /phi; aw.
have tphi: K1 = target phi by rewrite /phi; aw.
have fphi: function phi by apply: lf_function.
rewrite sphi tphi; apply: (shepherd_principle fphi).
move => tf; rewrite - tphi; move /Zo_P => [] /setP_P tfj ctf.
set K2:= Zo (functions I J) (fun f => image_of_fun f = tf).
have ->: inv_image_by_fun phi (singleton tf) = K2.
  set_extens t.
     move /(iim_fun_set1_P _ fphi) => []; rewrite - sphi /phi => t1; aw.
     move /Zo_P: t1 => [t1 t2] t3; apply /Zo_P;split => //.
  move => /Zo_P [t1 t2]; apply /(iim_fun_set1_P _ fphi); rewrite - sphi.
  have te1: inc t E1 by apply /Zo_P; rewrite t2.
  by rewrite /phi; aw.
rewrite ci - ctf.
have f1: finite_set I by red; rewrite - ci; apply /BnatP.
have f2: finite_set tf by red; rewrite ctf; apply /BnatP.
rewrite -(nbsurj_pr f1 f2); clear f1 f2.
apply /card_eqP.
exists (Lf restriction_to_image K2 (surjections I tf)); split;aw.
apply: lf_bijective.
    move => c /Zo_P [] /fun_set_P [qa qb qc] qd; apply /Zo_P.
    move: (restriction_to_image_fs qa) => qe;split => //; apply /fun_set_P.
    move: (proj1 qe) => f; split => //; rewrite /restriction_to_image.
    by rewrite /restriction2; aw.
    by rewrite /restriction2; aw.
  move => u v /Zo_P [] /fun_set_P [qa qb qc] qd.
  move => /Zo_P [] /fun_set_P [ra rb rc] rd sr.
  apply: function_exten => //; rewrite ? rb ? rc // => x xI.
  move: (f_equal (Vf ^~x) sr).
  move: (restriction_to_image_axioms qa) => h; rewrite restriction2_V //.
  move: (restriction_to_image_axioms ra) => h'; rewrite restriction2_V //.
  by rewrite rb - qb.
move => y /Zo_P [] /fun_set_P [qa qb qc] qd.
set f := Lf (Vf y) I J.
have fa: forall z, inc z I -> inc (Vf y z) J.
    rewrite -qb; move => z zi; apply: tfj; rewrite -qc; Wtac.
  have fb: function f by apply: lf_function.
  have sfi: source f = I by rewrite /f;aw.
  have fc: image_of_fun f = tf.
    set_extens t.
      move /(Vf_image_P1 fb); rewrite sfi; move => [u u1 ->]; rewrite /f; aw.
      Wtac.
    rewrite -qc => tt; move: (proj2 qd _ tt); rewrite qb; move => [u u1 u2].
    by apply /(Vf_image_P1 fb); rewrite sfi;ex_tac; rewrite /f;aw.
  have fd:inc f K2 by apply/ Zo_P; split => //;apply /fun_set_P;rewrite /f;red;aw.
  move: (proj1 (restriction_to_image_fs fb)) => ra.
  move: (restriction_to_image_axioms fb) => rb.
  have sr:source (restriction_to_image f) = source y by rewrite corresp_s sfi.
  ex_tac; apply: function_exten => //.
    by rewrite corresp_t fc.
  rewrite qb;move => t ts /=; rewrite restriction2_V // -? sfi // /f; aw.
Qed.

Definition Bell_number n := cardinal (partitions (Bint n)).

Lemma Bell_pr E :
  finite_set E ->
  cardinal (partitions E) =
  card_sumb (Bintc (cardinal E))
     (fun p => cardinal (partitionsx E p)).
Proof.
set X:= (partitions E).
set n := cardinal E; move /BnatP => nB.
set F := (Bintc n).
suff h: (forall x, inc x X -> inc (cardinal x) F).
  rewrite (card_partition_induced h) /card_sumb; apply f_equal; apply: Lg_exten.
  move => p pF /=; apply: f_equal; set_extens t.
    move => /Zo_P [] /Zo_P=> [[pa pb] pc]; apply /Zo_P;split => //.
  by move => /Zo_P [pa [pb pc]]; apply /Zo_P => //;split => //; apply /Zo_P.
move => x /Zo_P [] pa [[pb pd] pc]; apply /(BintcP nB).
have injf: injection (Lf rep x E).
  apply: lf_injective.
    by move => t tx; move: (rep_i (pc _ tx)) => h; rewrite - pb; union_tac.
  move => u v ux vx; case: (pd _ _ ux vx) => // bad sr.
  empty_tac1 (rep u).
      exact: (rep_i (pc _ ux)).
      rewrite sr;exact: (rep_i (pc _ vx)).
move: (incr_fun_morph injf); aw.
Qed.

Lemma Bell_pr1 n: inc n Bnat ->
  Bell_number n = card_sumb (Bintc n) (fun p => nbpart n p).
Proof.
move => nB.
have ce: cardinal (Bint n) = n by rewrite (card_Bint nB).
have fse: finite_set (Bint n) by red; rewrite ce; apply /BnatP.
by rewrite /Bell_number (Bell_pr fse) /nbpart ce.
Qed.

Lemma Bell_pr2 E: finite_set E ->
  cardinal (partitions E) = Bell_number (cardinal E).
Proof.
move => fse.
have nB: inc (cardinal E) Bnat by move: fse; move /BnatP.
rewrite (Bell_pr fse) (Bell_pr1 nB); rewrite /card_sumb; apply: f_equal.
apply: Lg_exten => p pn; rewrite nbpart_pr //.
Qed.

Lemma Bell_rec n : inc n Bnat ->
  Bell_number (succ n) =
  card_sumb (Bintc n) (fun k => (binom n k) *c (Bell_number k)).
Proof.
move => nB.
set E := Bint (succ n); set X := (partitions E).
set E' := (Bint n).
have nE: inc n E by apply: Bint_si.
have ce: cardinal E = succ n by rewrite (card_Bint (BS_succ nB)).
have ce1: cardinal E' = n by rewrite (card_Bint nB).
have see': sub E' E by apply:Bint_M.
pose fb p := select (fun s => inc n s) p.
have prb: forall p, inc p X -> inc n (fb p) /\ inc (fb p) p.
  move => t /Zo_P [_] [[pa pc] pb]; apply: (select_pr).
     move: nE; rewrite -pa; move /setU_P => [y sa sb]; ex_tac.
  move => x y xp nx yp ny; case: (pc _ _ xp yp) => // bad; empty_tac1 n.
have fcq: forall p, inc p X -> cardinal (fb p -s1 n) <=c n.
  move => p pX; move: (prb _ pX) => [pa pb].
  apply /(card_le_succ_succP); fprops.
  rewrite - (card_succ_pr2 pa) - ce; move /Zo_P: pX => [] /setP_P h _.
  move: (h _ pb) => /setP_P => h1; apply: (sub_smaller h1).
pose fc p := n -c cardinal (fb p -s1 n).
have fcp: forall p, inc p X-> inc (fc p) (Bintc n).
  by move => p pX; apply /(BintcP nB); apply: cdiff_le_symmetry; apply: fcq.
rewrite /Bell_number (card_partition_induced fcp) /card_sumb.
apply: f_equal; apply: Lg_exten => k /(BintcP nB) kn.
move: (BS_le_int kn nB) => kB.
rewrite (binom_symmetric nB kB kn).
rewrite (subsets_with_p_elements_pr nB (BS_diff k nB) ce1).
set E1 := Zo _ _; set K1 := subsets_with_p_elements _ _.
pose phi := Lf (fun z => (fb z -s1 n)) E1 K1.
have pc: forall c, inc c E1 -> inc (fb c -s1 n) K1.
  move => x /Zo_P [pa pb]; apply /Zo_P;split => //.
     apply /setP_P.
     move => t /setC1_P [pc pd]; apply /(BintP nB); split => //.
     move:(prb _ pa) => [_]; move: pa => /Zo_P [] /setP_P => sa _ sb.
     by move: (sa _ sb) => /setP_P => sc; apply /(BintsP nB); apply: sc.
  by rewrite -pb /fc double_diff //; apply: fcq.
have sphi: E1 = source phi by rewrite /phi; aw.
have tphi: K1 = target phi by rewrite /phi; aw.
have fphi: function phi by apply: lf_function.
rewrite sphi tphi; apply: (shepherd_principle fphi).
rewrite - tphi => S /Zo_P [] /setP_P sa sb.
have ->: (inv_image_by_fun phi (singleton S)) =
   Zo X (fun z => fb z -s1 n = S).
   set_extens t.
      move /(iim_fun_set1_P _ fphi); rewrite - sphi; move => [s1].
      by rewrite /phi; aw => s2; apply /Zo_P;split => //; move /Zo_P: s1 => [].
   move => /Zo_P [s1 s2]; apply /(iim_fun_set1_P _ fphi).
   have te1: inc t E1.
      by apply /Zo_P;split => //; rewrite /fc s2 sb double_diff.
   by rewrite - sphi /phi;split => //;aw.
have sc: E -s (S +s1 n) = E' -s S.
     set_extens t.
       move => /setC_P [te] /setU1_P h; apply /setC_P.
       case: (equal_or_not t n) => tn; first by case: h; right.
       split; last by move => h1; case: h; left.
       by apply /(BintP nB); split => //; apply /(BintsP nB).
     move => /setC_P [t1 t2]; apply /setC_P; split; first by apply: see'.
     by apply /setU1_P; case => // tn; move /(BintP nB) : t1 => [].
have sd: k = n -c cardinal S by rewrite sb double_diff.
pose E'':= (E -s (S +s1 n)).
have se: cardinal E'' = k.
  have fse': finite_set E' by apply /BnatP; rewrite (card_Bint nB).
  by rewrite /E'' sc (cardinal_setC4 sa fse') ce1 sd.
rewrite -/(Bell_number k) - se - Bell_pr2; last by apply/BnatP; rewrite se.
symmetry; apply/ card_eqP.
set A:= partitions E''; set B := Zo _ _.
pose f p := p +s1 (S +s1 n).
have pa: forall p, inc p A -> inc (f p) (powerset (powerset E)).
  move => p /Zo_P [p1 [[p2 p4] p3]]; apply /setP_P => t /setU1_P; case.
    move => tp; apply /setP_P => s st.
    move/setP_P: p1 => h1; move: (h1 _ tp) => h2; move/setP_P: h2 => h3.
    by move: (h3 _ st) => /setC_P [].
  move => ->; apply /setP_P => s /setU1_P; case; fprops.
  move => ->; apply :(Bint_si nB).
have pb: forall p, inc p A -> inc (f p) X.
  move => p pA; move: (pa _ pA) => pn; apply /Zo_P; split => //.
  move /Zo_P: pA => [_] [[p1 p3] p2]; split; last first.
    move => t /setU1_P; case; [apply: p2 | move => ->; exists n; fprops].
    split; first set_extens t.
      move => /setU_P [z tz zf]; move/setP_P: pn => h; move: (h _ zf).
      by move /setP_P; apply.
    move => te; case: (inc_or_not t (S +s1 n)) => h.
      by union_tac; apply /setU1_P; right.
    move: (setC_i te h); rewrite -/E'' -p1 => /setU_P [z za zb].
    by union_tac; apply /setU1_P; left.
  move => a b /setU1_P; case => pb /setU1_P; case => pd.
      by apply: p3.
     right; rewrite pd; move: (setU_s1 pb); rewrite p1 => h.
     by apply: disjoint_pr => s sx; move: (h _ sx) => /setC_P [].
   right; rewrite pb; move: (setU_s1 pd); rewrite p1 => h.
    by apply: disjoint_pr => s sx sy; move: (h _ sy) => /setC_P [].
  by rewrite pb pd; left.
have pd: forall p, inc p A -> fb (f p) = (S +s1 n).
  move => p pA; move: (pb _ pA) => h; move: (prb _ h) => [s1 s2].
  case /setU1_P: s2 => // h1.
  move /Zo_P: pA => [] /setP_P ha _; move: (ha _ h1) => /setP_P => hb.
  by move: (hb _ s1) => /setC_P [_] /setU1_P; case; right.
exists (Lf f A B); split; aw;apply: lf_bijective.
    move => p pA; apply /Zo_P;split; first by apply: pb.
    rewrite (pd _ pA); apply: setU1_K => ns; move: (sa _ ns).
    by move /(BintP nB) => [].
  move => u v uA vA sf.
   have aux: forall s, inc s A -> ~ inc (S +s1 n) s.
     move => s /Zo_P [] /setP_P h _ h1; move: (h _ h1) => /setP_P h2.
     have h3: inc n (S +s1 n) by fprops.
     by move: (h2 _ h3) => /setC_P [].
   by rewrite - (setU1_K (aux _ uA)) - (setU1_K (aux _ vA)) - /(f u) sf.
move => y /Zo_P [p1 p2]; move: (prb _ p1) => [p3 p4].
have aux: S +s1 n = fb y by rewrite - p2;apply: setC1_K.
exists (y -s1 (fb y)); last by symmetry;rewrite /f aux;apply: setC1_K.
have q1: inc (y -s1 fb y) (powerset (powerset E'')).
  apply /setP_P => t /setC1_P [] ta tb; apply /setP_P => s st; apply /setC_P.
  move /Zo_P: p1 => [] /setP_P ha [[q1 q3] q2]; split.
    by move: (ha _ ta) => /setP_P; apply.
  move => h; case: (q3 _ _ p4 ta); rewrite /disjoint => h1; first by case: tb.
  by empty_tac1 s; apply /setI2_P; split => //; rewrite - aux.
move /Zo_P: p1 => [_] [[q3 q5] q4].
apply /Zo_P;split => //; split; first split.
    move /setP_P: q1 => q2; set_extens t.
    by move /setU_P => [z za zb]; move: (q2 _ zb) => /setP_P; apply.
  move /setC_P => [t1 t2]; move: t1; rewrite -q3 => /setU_P [z z1 z2].
  by union_tac; apply /setC1_P;split => //; move => h; case: t2; rewrite aux -h.
by move => a b /setC1_P [s1 _] /setC1_P [s2 _]; apply: q5.
by move => s /setC1_P [sy _]; apply:q4.
Qed.


Definition derangements E :=
  Zo (permutations E) (fun z => forall x, inc x E -> Vf z x <> x).

Definition nbder n :=
  cardinal(derangements (Bint n)).

Lemma nbder_pr E: finite_set E ->
   cardinal (derangements E) = nbder (cardinal E).
Proof.
have aux: forall I J g f,
    bijection g -> source g = J -> target g = I ->
    inc f (derangements J) ->
    inc (g \co (f \co inverse_fun g)) (derangements I).
  move => I J g f big sg tg.
  move: (inverse_bij_fb big); set g1 := inverse_fun g => igb.
  move: (proj1 (proj1 big))(proj1(proj1 igb)) => fg fig.
  move => /Zo_P [] /Zo_P [] /fun_set_P [pa pb pc] pd pe.
  have qa: (f \coP g1) by rewrite /g1;red; aw;split => //; ue.
  have qb: bijection (f \co g1) by apply: compose_fb.
  have qc: (g \coP (f \co g1)) by split => //;aw; try fct_tac; ue.
  have qd: bijection (g \co (f \co g1)) by apply: compose_fb.
  have sg1: source g1 = I by rewrite /g1; aw.
  have qe: inc (g \co (f \co g1)) (permutations I).
     apply /Zo_P;split => //; apply /fun_set_P; split => //; aw;fct_tac.
  apply/ Zo_P; split => // => x xi => eq.
  move: (f_equal (Vf g1) eq).
  rewrite - sg1 in xi; aw; rewrite -/g1; set y:= Vf g1 x.
  have ye: inc y J by rewrite- sg - ifun_t /y /g1; Wtac; aw.
  have ysg: inc (Vf f y) (source g) by rewrite sg - pc; Wtac.
  rewrite (inverse_V2 big ysg); exact (pe _ ye).
move => fse; set n := cardinal E; set I :=Bint n.
have nB: inc n Bnat by apply /BnatP.
have : n = cardinal I by rewrite (card_Bint nB).
move/card_eqP => [g [big sg tg]]; apply /card_eqP.
pose c f := g \co (f \co (inverse_fun g)).
move: (inverse_bij_fb big); set g1 := inverse_fun g => igb.
move: (proj1 (proj1 big))(proj1(proj1 igb)) => fg fig.
exists (Lf c (derangements E) (derangements I)); split;aw.
apply: lf_bijective.
move => f.
    by apply: aux.
  move => u v /Zo_P [] /Zo_P [] /fun_set_P [pa pb pc] _ _.
  move => /Zo_P [] /Zo_P [] /fun_set_P [qa qb qc] _ _ sv.
  have ra: (u \coP g1) by rewrite /g1;red; aw;split => //; ue.
  have rb: function (u \co g1) by fct_tac.
  have rc: (g \coP (u \co g1)) by split => //;aw; ue.
  have ra': (v \coP g1) by rewrite /g1;red; aw;split => //; ue.
  have rb': function (v \co g1) by fct_tac.
  have rc': (g \coP (v \co g1)) by split => //;aw; ue.
  move: (fct_co_simpl_left rc rc' big sv) => sv1.
  exact: (fct_co_simpl_right ra ra' igb sv1).
move => y yv; set x := (g1 \co (y \co (inverse_fun g1))).
have sg1: source g1 = I by rewrite /g1; aw.
have tg1: target g1 = E by rewrite /g1; aw.
move: (aux _ _ _ _ igb sg1 tg1 yv); rewrite (ifun_involutive fg) => h; ex_tac.
move: yv => /Zo_P [] /Zo_P [] /fun_set_P [fy sy ty] _ _.
rewrite /c -/g1.
have pa: (y \coP g) by split => //; ue.
have pb: function (y \co g) by fct_tac.
have pc: g1 \coP (y \co g) by split; aw; ue.
have pd: (y \co g) \coP g1 by split; aw; ue.
have pe: g1 \coP ((y \co g) \co g1) by red;aw;split => //; try fct_tac; ue.
move: (composable_f_inv big) => pf.
rewrite - compfA // compfA // bij_right_inverse //.
rewrite - compfA // bij_right_inverse // tg - {2} sy compf_id_r //.
rewrite - ty compf_id_l //.
Qed.

Lemma nbder_0: nbder \0c = \1c.
Proof.
rewrite /nbder /derangements.
set E := (Bint \0c); set X:= Zo _ _.
set f := empty_function.
have EE: E = emptyset by exact Bint_co00.
move: empty_function_function => pa.
move: (pa) => [p1 p2 p3].
have bf: bijection f.
   split; split => //.
   by move => x y; rewrite p2 => /in_set0.
   by move => y; rewrite p3 => /in_set0.
have fp:inc f (permutations emptyset).
   by apply /Zo_P;split => //; apply /fun_set_P.
have fX: inc f X.
  by rewrite /X EE; apply /Zo_P; split => // x /in_set0.
have ->: X = singleton f.
   apply: set1_pr => // z /Zo_P [] /Zo_P [] /fun_set_P [sa sb sc] _ _.
   apply: function_exten => //.
      by rewrite sb EE.
     by rewrite sc EE.
   by move => t; rewrite sb EE => /in_set0.
by rewrite cardinal_set1.
Qed.

Lemma nbder_1: nbder \1c = \0c.
Proof.
rewrite /nbder;set E := derangements _.
suff: E = emptyset by move => ->; apply: cardinal_set0.
apply /set0_P => t /Zo_P [] /Zo_P [] /fun_set_P [ff sf tf] _ pf.
move:Bint_co01 => [pa pb].
move: (pf _ pa) => f0.
by rewrite - sf in pa; move: (Vf_target ff pa); rewrite tf pb => /set1_P.
Qed.

Lemma Exercise5_8a n: inc n Bnat ->
  factorial n = card_sumb (Bintc n) (fun k =>
    binom n k *c nbder k).
Proof.
move => nB.
set I := (Bint n).
have caI : cardinal I = n by rewrite (card_Bint nB).
have fsi: finite_set I by red; rewrite caI; apply /BnatP.
move: (number_of_permutations fsi); rewrite - caI => <-.
pose g f := Zo I (fun x => Vf f x <> x).
pose Xk k := Zo (permutations I) (fun z => cardinal (g z) = k).
set X := Lg (Bintc n) Xk.
have X1: fgraph X by rewrite /X; fprops.
have X2: mutually_disjoint X.
  red;rewrite /X; bw => i j ip jp; bw;mdi_tac nij => u ua ub; case: nij.
  by move: ua ub => /Zo_P [_ <- ] /Zo_P [_ <-].
have X3: (unionb X) = (permutations I).
   rewrite /X;set_extens t.
     move /setUb_P; bw; move => [y yp]; bw; move /Zo_P => [p1 p2] //.
   have sa: inc (cardinal (g t)) (Bintc n).
     have h: sub (g t) I by apply: Zo_S.
     apply /BintcP => //; rewrite - caI; apply: (sub_smaller h).
   move => ti; apply /setUb_P; bw;exists (cardinal (g t)) => //.
   rewrite /Xk; bw;apply /Zo_P;split => //.
move: (csum_pr4 X2); rewrite X3 => ->.
rewrite {1} /X /card_sumb caI; bw; apply: f_equal; apply: Lg_exten.
move => k kn; rewrite /X; bw; move/(BintcP nB): kn => kn;clear X X1 X2 X3.
move: (BS_le_int kn nB) => kB.
rewrite(subsets_with_p_elements_pr nB kB caI).
set K := (subsets_with_p_elements k I).
pose phi := Lf g (Xk k) K.
have sphi: (Xk k) = source phi by rewrite /phi; aw.
have ->: K = target phi by rewrite /phi; aw.
have ta: lf_axiom g (Xk k) K.
  by move => f /Zo_P [p1 p2]; apply/Zo_P;split => //; apply/setP_P; apply: Zo_S.
have fphi: function phi by apply: lf_function.
rewrite sphi; apply: (shepherd_principle fphi).
rewrite {1} /phi; aw; move => x xK.
set W := (inv_image_by_fun phi (singleton x)).
have kp: forall f, inc f W <-> inc f (Xk k) /\ g f = x.
  move => f; split.
    by move/(iim_fun_set1_P _ fphi); rewrite - sphi /phi; move => [h];aw => h1. move => [pa pb]; apply/(iim_fun_set1_P _ fphi).
  have fsp: inc f (source phi) by rewrite - sphi.
  by rewrite /phi;aw.
move: (xK) => /Zo_P [] /setP_P sxi cx.
pose r f := Lf (Vf f) x x.
have pa: forall f, inc f W ->
   [/\ lf_axiom (Vf f) x x,
     (forall t, inc t x -> Vf (r f) t = Vf f t),
    (forall t, inc t (I -s x) -> Vf f t = t) &
   inc (r f) (derangements x)].
  move => f /kp [] /Zo_P [] /Zo_P [] /fun_set_P [ff sf tf] bf fp gf.
  have lfa: lf_axiom (Vf f) x x.
     move => s st; move: (st); rewrite - gf => /Zo_P [si siv].
     have ax: inc (Vf f s) I by rewrite - tf; Wtac.
     apply /Zo_P;split => // => sv; rewrite - sf in si ax.
     by move:(bij_inj bf ax si sv).
  have sv: forall t, inc t x -> Vf (r f) t = Vf f t.
     move => t tx; rewrite /r; aw.
  have sv1:(forall t, inc t x -> Vf (r f) t <> t).
    by move => t tx; rewrite (sv _ tx); move: tx; rewrite - gf => /Zo_P [].
  have sv2: (forall t : Set, inc t (I -s x) -> Vf f t = t).
   by move => t /setC_P [ti tx]; ex_middle fx;case: tx;rewrite - gf; apply /Zo_P.
  rewrite /r;split => //; apply /Zo_P;split => //.
  apply /Zo_P;split => //.
    by apply /fun_set_P;split;aw => //; apply:lf_function.
  apply: lf_bijective => //.
    by move => u v ux vx; apply: (bij_inj bf); rewrite sf; apply: sxi.
  move => y yx.
  move: (sxi _ yx); rewrite -tf => ytf.
  move: (bij_surj bf ytf); rewrite sf; move => [z za zb]; exists z => //.
  by ex_middle zx; rewrite - (sv2 _ (setC_i za zx)) zb.
have ->: nbder k = cardinal (derangements x).
   have fsx: finite_set x by red; rewrite cx; apply /BnatP.
   by rewrite (nbder_pr fsx) cx.
apply /card_eqP; exists (Lf r W (derangements x)); split;aw.
apply:lf_bijective.
    by move => t ts; move: (pa _ ts) => [_ _ _].
  move => u v uw vw sr.
  move: (pa _ uw) (pa _ vw) => [_ p1 p2 _] [_ q1 q2 _].
  move: uw => /kp [] /Zo_P [] /Zo_P [] /fun_set_P [f1 f2 f3] _ _ _.
  move: vw => /kp [] /Zo_P [] /Zo_P [] /fun_set_P [f1' f2' f3'] _ _ _.
  apply: function_exten => //; try ue.
  move => t ts; case: (inc_or_not t x) => tx.
    by rewrite - (p1 _ tx) - (q1 _ tx) sr.
  by rewrite f2 in ts; move : (setC_i ts tx) => h; rewrite (p2 _ h) (q2 _ h).
move => y yd.
move: yd => /Zo_P [] /Zo_P [] /fun_set_P [y1 y2 y3] y4 y5.
set f := Lf (fun z => (Yo (inc z x) (Vf y z) z)) I I.
have sa: forall z, inc z I -> inc ((Yo (inc z x) (Vf y z) z)) I.
  move => z zi; Ytac zx => //;apply: sxi; rewrite - y3; Wtac.
have ff: function f by apply: lf_function.
have gfx: g f = x.
   set_extens t.
     by move /Zo_P => [t1 t2]; ex_middle ntx; case: t2; rewrite /f; aw; Ytac0.
   move => tx; move: (sxi _ tx) => ti.
   by apply /Zo_P;split => //;rewrite /f; aw; Ytac0; apply: y5.
have bf: bijection f.
  apply: lf_bijective.
     move => s; apply: sa.
  move => u v ui vi; case: (inc_or_not u x) => ux; Ytac0.
       case: (inc_or_not v x) => vx; Ytac0.
         by apply (bij_inj y4); rewrite y2.
       rewrite -y2 in ux; move: (Vf_target y1 ux); rewrite y3.
       by move => s1 s2; case: vx; rewrite - s2.
    case: (inc_or_not v x) => vx; Ytac0 => //.
    rewrite -y2 in vx; move: (Vf_target y1 vx); rewrite y3.
    by move => s1 s2; case: ux; rewrite s2.
  move => z zi; case: (inc_or_not z x).
    rewrite - {1} y3 => zy; move: (bij_surj y4 zy) => [t ]; rewrite y2.
    by move => tx <-; move: (sxi _ tx) => ti; ex_tac; Ytac0.
   by move => zx; ex_tac; Ytac0.
have fp: inc f (permutations I).
   apply /Zo_P;split => //; apply /fun_set_P; rewrite /f; red;aw;split => //.
have rfy: r f = y.
  symmetry;rewrite /r/f.
  have aux:
     lf_axiom (Vf (Lf (fun z0 : Set => Yo (inc z0 x) (Vf y z0) z0) I I)) x x.
    move => t tx;move: (sxi _ tx) => ti; aw;Ytac0; rewrite - y3; Wtac.
  apply: function_exten; aw; first by apply lf_function => //.
  by rewrite y2;move => s sx /=; move: (sxi _ sx) => si; aw; Ytac0.
by exists f => //; apply /kp;split => //; apply /Zo_P;split => //; rewrite gfx.
Qed.

Lemma nbder_pr2 n: inc n Bnat ->
   nbder (succ (succ n)) = (succ n) *c (nbder n +c nbder (succ n)).
Proof.
move => nB.
move: (BS_succ nB) => snB.
move: (Bint_pr4 snB).
set I :=Bint (succ n); set I' := Bint (succ (succ n)).
move => [pa pb].
have pc: inc (succ n) I' by apply:Bint_si.
have ci: cardinal I= succ n by apply:(card_Bint snB).
set G1 := (derangements I').
pose phi := Lf (Vf ^~(succ n)) G1 I.
have sp: G1 = source phi by rewrite /phi; aw.
have tp: I = target phi by rewrite /phi; aw.
have lfa: lf_axiom (Vf^~(succ n)) G1 I.
  move => f /Zo_P [] /Zo_P [] /fun_set_P [ta tb tc] td te.
  move: (te _ pc) => bad; move: pc; rewrite -tb => pc.
  by move: (Vf_target ta pc); rewrite tc -pa; case /setU1_P.
have fphi: function phi by apply: lf_function.
have ci': cardinal I'= succ (succ n) by apply:(card_Bint (BS_succ snB)).
have <-: cardinal (source phi) = nbder (succ (succ n)).
    rewrite - sp - ci'; apply:nbder_pr; red; rewrite ci'; apply /BnatP; fprops.
rewrite - {1} ci tp;apply:(shepherd_principle fphi).
rewrite {1} /phi; aw; move => x xK.
set G2 := Zo G1 (fun f => Vf f (succ n) = x).
have ->: inv_image_by_fun phi (singleton x) = G2.
   set_extens t.
    move/(iim_fun_set1_P _ fphi); rewrite - sp;move => [ts].
      rewrite /phi /G2; aw => ->; apply /Zo_P;split => //.
  by move => /Zo_P [tg1 <-]; apply /(iim_fun_set1_P _ fphi); rewrite /phi; aw.
set G3 := Zo G2 (fun f => Vf f x = (succ n)).
have sg3: sub G3 G2 by apply: Zo_S.
have h0: succ n <> x by move => h1; case: pb; rewrite h1.
have fi: finite_set I' by red; rewrite ci'; apply /BnatP; fprops.
have xi': inc x I' by rewrite - pa; fprops.
rewrite (cardinal_setC2 sg3) - csum2_pr2a - csum2_pr2b;congr (_ +c _).
  set K := I -s1 x.
  have cK: n = cardinal K.
    by apply: succ_injective1; fprops; rewrite - ci (card_succ_pr2 xK).
  have fsk: finite_set K by red; rewrite - cK; apply /BnatP.
  rewrite cK - (nbder_pr fsk); apply /card_eqP.
  exists (Lf (fun f => (restriction2 f K K)) G3 (derangements K)).
    split;aw.
  have ski': sub K I' by rewrite -pa;move => t /setC_P [ti _]; fprops.
  have pd: forall f, inc f G3 -> restriction2_axioms f K K.
     move => f /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /fun_set_P
        [qa qb qc] qd qe qf qg.
     have ksf: sub K (source f) by ue.
     red; rewrite qb qc ;split => // t /(Vf_image_P qa ksf) [u uk ->].
     move: (ksf _ uk) => usf; move: (Vf_target qa usf); rewrite qc -pa.
     have xsf: inc x (source f) by rewrite qb -pa; fprops.
     have nsf: inc (succ n) (source f) by rewrite qb -pa; fprops.
     move /setC1_P: uk => [ui ux]; case /setU1_P => h.
        apply /setC1_P;split => // => h1; rewrite -h1 in qf.
        by move: (bij_inj qd nsf usf qf) => us; case: pb; rewrite us.
     by rewrite -h in qg; move: (bij_inj qd xsf usf qg) => xu; case: ux.
  apply: lf_bijective.
      move => f fg3; move: (pd _ fg3) => pe.
      set g := (restriction2 f K K).
      move: (restriction2_prop pe) => p0.
      have gs: inc g (functions K K) by apply /fun_set_P.
      move: p0 => [p1 p2 p3].
      move: fg3 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /fun_set_P
        [qa qb qc] qd qe qf qg.
      move: (restriction2_fi (proj1 qd) pe) => ir.
      apply /Zo_P; split; first (apply/Zo_P => //; split => //).
        apply:bijective_if_same_finite_c_inj; rewrite ? p2 ? p3 //.
      move => t tK; rewrite (restriction2_V pe tK); apply: qe; fprops.
    move => u v ug3 vg3; move: (pd _ ug3) (pd _ vg3) => pe pe' sr.
    move: ug3 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /fun_set_P
      [qa qb qc] qd qe qf qg.
    move: vg3 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /fun_set_P
      [qa' qb' qc'] qd' qe' qf' qg'.
    apply: function_exten; rewrite ? qb' ? qc' //.
    rewrite qb -pa => t; case /setU1_P ; last by move => ->; rewrite qf.
    move => ti; case: (equal_or_not t x); first by move => ->; rewrite qg.
    move => tx; move /setC1_P: (conj ti tx) => tK.
    by rewrite - (restriction2_V pe tK) - (restriction2_V pe' tK) sr.
  move => y ydK.
  move: ydK => /Zo_P [] /Zo_P [] /fun_set_P [fy sy ty] biy nfy.
  pose f z := Yo (z = succ n) x (Yo (z = x) (succ n) (Vf y z)).
  have f1: f (succ n) = x by rewrite /f; Ytac0; Ytac0.
  have f2: f x = (succ n) by rewrite /f; Ytac0; Ytac0.
  have f3: forall t, inc t K -> f t = Vf y t.
  move => t /setC1_P [ti tk]; rewrite /f; Ytac0; Ytac h => //; case: pb; ue.
  have f4: forall t, inc t K -> inc (f t) K.
       move => t tk; rewrite (f3 _ tk); rewrite - ty; Wtac.
  have f5: lf_axiom f I' I'.
      move => t; rewrite -pa; case: (equal_or_not t x).
        by move ->; rewrite f2; fprops.
      move => tx; case/setU1_P => ta; last by rewrite ta f1; fprops.
      by rewrite pa; apply: ski'; apply: f4;apply /setC1_P.
    have f6: function (Lf f I' I') by apply:lf_function.
    have f7: restriction2_axioms (Lf f I' I') K K.
       have h: sub K (source (Lf f I' I')) by aw.
       red; aw;split => // t; move /(Vf_image_P f6 h) => [u uK].
       by aw; fprops => ->; apply: f4.
    move: (restriction2_prop f7) => [p1 p2 p3].
    have f8: (restriction2 (Lf f I' I') K K) = y.
       apply: function_exten; rewrite ? p2 ? p3 //.
       move => t tk /=; rewrite (restriction2_V f7); aw; fprops.
    have f9: forall t, inc t I' -> f t <> t.
      move => t; rewrite -pa; case: (equal_or_not t x).
        move => -> _; rewrite f2 //.
      move => tx; case /setU1_P; last by move => ->; rewrite f1; fprops.
      move => ti; move /setC1_P: (conj ti tx) => tK.
      by rewrite (f3 _ tK);apply: nfy.
   have f10: inc (Lf f I' I') (permutations I').
     apply /Zo_P; split; first by apply /fun_set_P; red;aw;split => //.
     apply:bijective_if_same_finite_c_surj; aw; apply /lf_surjective => //.
     move => z; rewrite - pa; case /setU1_P; last first.
       move => ->; exists x;fprops.
     case: (equal_or_not z x)=> zx zi.
         by rewrite zx; exists (succ n); fprops.
     move /setC1_P: (conj zi zx); rewrite -/K - ty => yt.
     move: (bij_surj biy yt) => [w]; rewrite sy => wK <-.
     by rewrite - (f3 _ wK); exists w=> //; rewrite pa; apply: ski'.
  exists (Lf f I' I')=> //; apply /Zo_P; aw => //; split => //.
  apply /Zo_P; aw;split => //.
  by apply /Zo_P;split => // => t ti; aw; apply: f9.
set G4 := Zo G2 (fun f => Vf f x <> succ n).
have ->: (G2 -s G3) = G4.
  set_extens t.
    by move /setC_P => [tg2] /Zo_P p3; apply /Zo_P;split => // h; case: p3.
  by move => /Zo_P [p1 p2]; apply /setC_P;split => // ; move => /Zo_P [q1 q2].
pose g f := fun z => Yo (z = Vf (inverse_fun f) (succ n)) x (Vf f z).
pose g1 f := Lf (g f) I I.
have pd: forall f (y:= Vf (inverse_fun f) (succ n)), inc f G4 ->
      [/\ Vf f y = succ n, inc y I, (g f y) = x,
      (forall t, t <> y -> (g f t) = Vf f t) &
      (forall z, inc z I -> inc (g f z) I)].
  move => f y /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [].
  move /fun_set_P => [ff sg tf] bf nfp fn fx.
  move:(inverse_bij_fb bf) => ifb.
  have stf: inc (succ n) (target f) by rewrite tf -pa; fprops.
  have ysf: inc y (source f).
     by move: (Vf_target (proj1 (proj1 ifb))); aw; apply.
  have f1: Vf f y = succ n by rewrite /y inverse_V //.
  have yI: inc y I.
     rewrite sg in ysf; move: (nfp _ ysf) => yy.
     by move: ysf; rewrite -pa; case /setU1_P => // ysn; case: yy; rewrite f1.
  have f2: x <> y by dneg w; ue.
  have f3: (g f y) = x by rewrite /g /y; Ytac0.
  have f4: forall t, t <> y -> (g f t) = Vf f t.
    by move => t; rewrite /y /g => ty; Ytac0.
  have f5: (forall z, inc z I -> inc (g f z) I).
    move => z zI; case: (equal_or_not z y); first by move => ->; rewrite f3.
    move => zy; rewrite (f4 _ zy).
    have zsi: inc z (source f) by rewrite sg -pa; fprops.
    move: (Vf_target ff zsi); rewrite tf - pa; case /setU1_P => //.
    by move => h; rewrite -h in f1; case: zy; rewrite (bij_inj bf ysf zsi f1).
  done.
have fsi: finite_set I by red; rewrite ci; apply /BnatP.
move: (nbder_pr fsi); rewrite ci => <-.
apply /card_eqP; exists (Lf g1 G4 (derangements I)).
split; aw; apply: lf_bijective.
    move => f fg4; move: (pd _ fg4).
    set y := (Vf (inverse_fun f) (succ n)); move=> [f1 yI f3 f4 f5].
    move: fg4 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [].
    move /fun_set_P => [ff sg tf] bf nfp fn fx.
    have f2: x <> y by dneg w; ue.
    have f6: function (g1 f) by apply /lf_function.
    have f7: bijection (g1 f).
      rewrite /g1.
      apply:bijective_if_same_finite_c_surj; aw; apply /lf_surjective => //.
      move => t tI; have ti': inc t (target f) by rewrite tf -pa; fprops.
      move: (bij_surj bf ti'); rewrite sg; move => [u ui uv].
      rewrite -pa in ui;case /setU1_P: ui; last first.
      move => h; exists y => //; rewrite f3 - uv h fn => //.
      by move => ui; ex_tac; rewrite f4 // => uy; case: pb; rewrite -f1 - uy uv.
    have f8: inc (g1 f) (permutations I).
      by apply /Zo_P;split => //; rewrite /g1;apply /fun_set_P;red;aw.
    apply /Zo_P; split => // t ti; case: (equal_or_not t y).
      by move => ty; rewrite /g1; aw; rewrite ty f3.
    move => ty; rewrite /g1; aw; rewrite (f4 _ ty).
    apply: nfp; rewrite -pa; fprops.
  move => u v ug4 vg4 sg1.
  move: (ug4) => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [].
  move /fun_set_P => [ff sg tf] bf nfp fn fx.
  move: (vg4) => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [].
  move /fun_set_P => [ff' sg' tf'] bf' nfp' fn' fx'.
  apply: function_exten; rewrite ? sg ?sg' ? tf' //.
  move => t; rewrite - pa; case /setU1_P; last by move => ->; rewrite fn fn'.
  move => tI.
  move: (pd _ ug4) (pd _ vg4).
  set y := (Vf (inverse_fun u) (succ n)); move=> [f1 yI f3 f4 f5].
  set y' := (Vf (inverse_fun v) (succ n)); move=> [f1' yI' f3' f4' f5'].
  move: (f_equal (fun z => Vf z t) sg1); rewrite /g1; aw.
  have tsn: t <> succ n by move => h; case: pb; rewrite -h.
  have i1: Vf v (succ n) <> Vf v t.
    have tsv: inc t (source v) by rewrite sg' - pa; fprops.
    have nsv: inc (succ n) (source v) by rewrite sg' - pa; fprops.
    by move => h; case: tsn; rewrite (bij_inj bf' nsv tsv h).
  have i2: Vf u (succ n) <> Vf u t.
    have tsv: inc t (source u) by rewrite sg - pa; fprops.
    have nsv: inc (succ n) (source u) by rewrite sg - pa; fprops.
    by move => h; case: tsn; rewrite (bij_inj bf nsv tsv h).
  case: (equal_or_not t y) => ty.
     rewrite {1 3} ty f3 f1.
    case: (equal_or_not t y'); first by move => ->; rewrite f1'.
    by move => ty'; rewrite (f4' _ ty') - fn'.
  rewrite (f4 _ ty); case: (equal_or_not t y') => ty'; last by rewrite f4'.
  rewrite ty' f3' f1' - fn - ty' => h; by case: i2.
move => y /Zo_P [] /Zo_P [] /fun_set_P [fy sy ty] biy dy.
set xx := Vf (inverse_fun y) x.
 move:(inverse_bij_fb biy) => iyb.
have xty: inc x (target y) by ue.
have xxsf: inc xx (source y).
  by move: (Vf_target (proj1 (proj1 iyb))); aw; rewrite ty; apply.
have xxns: xx <> succ n by move => h; case: pb; rewrite -h - sy.
have f1: Vf y xx = x by rewrite /xx inverse_V //.
pose f z := Yo (z = succ n) x (Yo (z = xx) (succ n) (Vf y z)).
have f2: f (succ n) = x by rewrite /f; Ytac0; Ytac0.
have f3: f xx = (succ n) by rewrite /f; Ytac0; Ytac0.
have f4: forall t, t <> succ n -> t <> xx -> f t = Vf y t.
  by move => t t1 t2; rewrite /f; Ytac0; Ytac0.
have f5: f x <> succ n.
  rewrite /f; Ytac0; Ytac xa; first by case: (dy _ xK); rewrite xa f1.
  move => h; case: pb; rewrite -h - ty; Wtac.
have f6: forall t, inc t I' -> inc (f t) I'.
   move => t; rewrite -pa => ti; case: (equal_or_not t (succ n)) => tn.
      rewrite tn f2; fprops.
   case: (equal_or_not t xx) => txx.
      rewrite txx f3; fprops.
   rewrite (f4 _ tn txx); apply /setU1_P; left.
   rewrite -ty; Wtac; rewrite sy; case /setU1_P: ti => //.
have f7: function (Lf f I' I') by apply /lf_function.
have f8: bijection (Lf f I' I').
   apply:bijective_if_same_finite_c_surj; aw; apply /lf_surjective => //.
   move => t; rewrite -pa => /setU1_P; case; last first.
     move => ->; exists xx=> //; rewrite - sy;fprops.
   rewrite - ty => tty; move: (bij_surj biy tty) => [a asy av].
   have asn: a <> succ n by move => h; case: pb; rewrite -h - sy.
   case: (equal_or_not a xx); last first.
      by move =>axx; rewrite ty - sy; exists a;fprops; rewrite -av f4.
   by move => ax; exists (succ n); fprops;rewrite f2 - av ax f1.
have f9: inc (Lf f I' I') G1.
  apply /Zo_P; split; first by apply /Zo_P;split => //;apply /fun_set_P;red;aw.
  move => t ti;aw;
  case: (equal_or_not t (succ n)) => tn; first by rewrite tn f2; fprops.
  case: (equal_or_not t xx) => tx; first by rewrite tx f3; fprops.
  by rewrite (f4 _ tn tx); apply: dy; move: ti; rewrite -pa; case /setU1_P.
have f10: inc (Lf f I' I') G4 by apply /Zo_P; aw;split => //; apply /Zo_P; aw.
have II: sub I I' by rewrite -pa => t ti; fprops.
have f11: Vf (inverse_fun (Lf f I' I')) (succ n) = xx.
  have xxI': inc xx I' by apply: II; rewrite - sy.
  have ->: succ n = Vf (Lf f I' I') xx by aw.
  rewrite inverse_V2 //; aw.
have f12: lf_axiom (g (Lf f I' I')) I I.
  move => t ti; move: (II _ ti) => ti'; rewrite /g; aw;rewrite f11.
  Ytac aux; fprops; rewrite - ty; rewrite (f4 _ _ aux); try Wtac.
  by move => tn; case: pb; rewrite -tn.
have f13: function (Lf (g (Lf f I' I')) I I) by apply: lf_function.
ex_tac; rewrite /g1; apply: function_exten; aw.
rewrite sy => t ti; move: (II _ ti) => ti';rewrite /g;aw.
rewrite f11; Ytac aa ; rewrite ? aa //; rewrite f4//.
by move => tn; case: pb; rewrite -tn.
Qed.

Lemma nbder_pr3 f (g := fun n => (succ n) *c (f n)):
  (f \0c = \1c) -> f \1c = \0c ->
  (forall n, inc n Bnat ->
    f (succ (succ n)) = (succ n) *c (f n +c f (succ n))) ->
  (forall n, inc n Bnat -> (even_int n) -> f n <> \0c)
  /\
  (forall n, inc n Bnat ->
     f (succ n) = Yo (even_int n) (cpred (g n)) (succ (g n))).
Proof.
move => pa pb pc.
move: succ_zero => s0.
move: BS1 => bs1.
have pd': forall n, inc n Bnat -> inc (f n) Bnat /\ inc (f (succ n)) Bnat.
  apply: cardinal_c_induction; first by rewrite s0 pa pb;split;fprops.
  move => n nB [hr1 hr2]; split => //; rewrite(pc _ nB); fprops.
have pd: (forall n, inc n Bnat -> inc (f n) Bnat).
  move => n nb; exact (proj1 (pd' _ nb)).
have pe: (forall n : Set, inc n Bnat -> f (succ (succ n)) <> \0c).
  apply: cardinal_c_induction; first by rewrite (pc _ BS0) s0 pa pb; aw; fprops.
  move => n nB h; move: (BS_succ nB) => h1; rewrite (pc _ h1).
  move: (cpred_pr (pd _ (BS_succ h1)) h) => [pg ->].
  rewrite (csum_via_succ _ pg);apply: cprod2_nz; apply: succ_nz.
have pf: (forall n : Set, inc n Bnat -> even_int n -> f n <> \0c).
  move => n nB en; case: (equal_or_not n \0c).
    move => ->; rewrite pa; fprops.
  move => nz; move: (cpred_pr nB nz) => []; set p := (cpred n) => q1 q2.
  case: (equal_or_not p \0c) => pz.
    by case: odd_one => [] _; rewrite - succ_zero - pz - q2.
  move: (cpred_pr q1 pz) => [pp]; rewrite q2 => ->; fprops.
split; first by exact.
apply: cardinal_c_induction.
  have c1: cardinalp \1c by fprops.
  move: even_zero => h; Ytac0; rewrite /g pa s0 pb -(cpred_pr2 BS0) s0; aw.
move => n nB Hrec.
have snB: inc (succ n) Bnat by fprops.
rewrite (pc _ nB) cprod_sumDl.
set sn := succ n.
have sa: sn +c \1c = succ sn by rewrite Bsucc_rw.
have ->: Yo (even_int sn) (cpred (g sn)) (succ (g sn)) =
   (Yo (even_int sn) (cpred (f sn)) (succ (f sn)))
   +c (sn *c f sn).
   rewrite /g - sa cprod_sumDr csumC (cprod1l (CS_Bnat (pd _ snB))).
   Ytac ok; Ytac0; last by rewrite (csum_via_succ1 _ (pd _ snB)) //.
   case: (equal_or_not (f sn) \0c) => tz.
     by rewrite tz cprod0r (bsum0r BS0) /cpred setU_0 (bsum0r BS0).
   move: (cpred_pr (pd _ snB) tz) => [ta tb].
   rewrite {1} tb csum_via_succ1 // cpred_pr1 //; fprops.
congr (_ +c (sn *c f sn)).
move: (even_odd_succ n) => [qa qb].
rewrite Hrec /g -/sn.
case: (p_or_not_p (even_int n)) => en.
  move: (qa en) => [_] nesn; Ytac0; Ytac0.
  have gnz : sn *c f n <> \0c.
    apply: cprod2_nz; [apply: succ_nz | exact (pf _ nB en)].
  by move: (cpred_pr (BS_prod snB (pd _ nB)) gnz)=> [_].
have on: odd_int n by split.
move: (qb on) => nesn; Ytac0; Ytac0; rewrite cpred_pr1; fprops.
Qed.

Lemma nbder_pr4 n (g := fun n => (succ n) *c (nbder n)):
 inc n Bnat -> nbder (succ n) = Yo (even_int n) (cpred (g n)) (succ (g n)).
Proof.
apply:(proj2 (nbder_pr3 (f:= nbder) nbder_0 nbder_1 nbder_pr2)).
Qed.