Library sset16

Theory of Sets : Ordinals

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


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

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

Module NumberSums.

Enumerating a finite set of integers

Definition nth_more K S := S +s1 intersection (K -s S).
Definition nth_elts K := induction_term (fun _ S => nth_more K S) emptyset.

Lemma nth_set0 x (y := intersection x) : x = emptyset -> y = \0c.
Proof. by rewrite /y;move => ->; rewrite setI_0. Qed.

Lemma nth_set1 x (y := intersection x) :
  sub x Bnat -> nonempty x ->
  (inc y x /\ forall z, inc z x -> y <=c z).
Proof.
move => sB xnz.
have osx: ordinal_set x by move => i /sB /Bnat_oset.
move:(ordinal_setI xnz osx); rewrite -/y => yx; split => //.
move => z zx.
move: (CS_Bnat (sB _ yx)) (CS_Bnat (sB _ zx)) => sa sb.
by split => // t; move/(setI_P xnz); apply.
Qed.

Lemma nth_set2 K S: sub K S -> nth_more K S = S +s1 \0c.
Proof. by move => h; rewrite /nth_more (setC_T h) setI_0. Qed.

Lemma nth_set3 K: nth_more K K = K +s1 \0c.
Proof. by apply:nth_set2. Qed.

Definition segment_nat K S:=
  sub S K /\ (forall i j, inc i S -> inc j (K -s S) -> i <c j).

Lemma nth_set4 K S (S':= nth_more K S) (x:= intersection (K -s S)):
   sub K Bnat -> segment_nat K S -> S <> K ->
   [/\ segment_nat K S', inc x (S' -s S) & cardinal S' = succ (cardinal S)].
Proof.
move => KB [sa sb sc].
have sd:=(setC_ne (conj sa sc)).
have se:=(sub_trans (@sub_setC K S) KB).
move:(nth_set1 se sd); rewrite -/x; move => [/setC_P [xK xS] xm].
split; first split.
+ by move => t /setU1_P; case; [move /sa | move => ->].
+ move => i j /setU1_P iv /setC_P [jK /setU1_P jv].
  have aux: inc j (K -s S) by apply/setC_P; split => //;dneg js; left.
  case iv; first by move => iS; apply: sb => //.
  by rewrite -/x => ->; split; [ apply: xm | dneg h; right].
+ by apply/setC_P; split; [ apply:setU1_1 | ].
+ by rewrite card_succ_pr.
Qed.

Lemma nth_elts0 K: nth_elts K \0c = emptyset.
Proof. by apply:induction_term0. Qed.

Lemma nth_elts_succ K n:
 inc n Bnat -> nth_elts K (succ n) = nth_more K (nth_elts K n).
Proof. apply:induction_terms. Qed.

Lemma nth_set5 K n (S:= nth_elts K n):
   inc n Bnat -> sub K Bnat -> n <=c cardinal K ->
   (segment_nat K S /\ cardinal S = n).
Proof.
rewrite /S => nB kB;move: n {S} nB; apply: cardinal_c_induction.
  move => _; rewrite nth_elts0 cardinal_set0; split => //; split=> i.
    by move/in_set0.
  by move => j /in_set0.
move => n nB Hrec snk.
rewrite /nth_elts (induction_terms _ _ nB) -/(nth_elts K n).
move:(Hrec (card_leT (card_le_succ nB) snk)) => [sa sb].
case (equal_or_not (nth_elts K n) K) => nsK.
  by move: (proj2 (card_lt_leT (card_lt_succ nB) snk)); rewrite - nsK sb.
by move: (nth_set4 kB sa nsK); rewrite sb; move => [ua _ ub].
Qed.

Lemma nth_set6 K (n:= cardinal K):
   inc n Bnat -> sub K Bnat -> (nth_elts K n) = K.
Proof.
move => nB kB.
move: (nth_set5 nB kB (card_leR (CS_Bnat nB))) => [[sa _] sb].
have fsk: finite_set K by apply /BnatP.
move: (cardinal_setC4 sa fsk); rewrite sb cdiff_n_n.
by move /cardinal_nonemptyset => /empty_setC h; apply: extensionality.
Qed.

Lemma nth_set_M K n m:
  inc n Bnat -> m <=c n -> sub (nth_elts K m) (nth_elts K n).
Proof.
move => nB mn.
rewrite - (cdiff_pr mn).
move:(BS_diff m nB); set k:= (n -c m) => kB.
move:(BS_le_int mn nB) => mB; move: k kB;clear n mn nB.
apply: cardinal_c_induction; first by rewrite (csum0r (CS_Bnat mB)).
move => n nB hrec.
rewrite (csum_via_succ _ nB) (nth_elts_succ _ (BS_sum mB nB)).
apply /(sub_trans hrec) /subsetU2l.
Qed.

Definition nth_elt K n := union (nth_elts K (succ n) -s nth_elts K n).

Lemma nth_set7 K n (S:= (nth_elts K n)) (x:= nth_elt K n) :
   inc n Bnat -> sub K Bnat -> n <c cardinal K ->
   [/\ inc x (K -s S), inc x (nth_elts K (succ n)),
       forall y, inc y (K -s S) -> x <=c y
     & forall y, inc y S -> y <c x].
Proof.
move => nB KB h1.
have [[SK sw] cs1]:= (nth_set5 nB KB (proj1 h1)).
have pa: sub (K -s S) Bnat by move => t/setC_P [/ KB h _].
case: (emptyset_dichot (K -s S)) => nek.
  by case: (proj2 h1); rewrite - cs1 {2} (extensionality (empty_setC nek) SK).
have h2: succ n <=c cardinal K by apply /(card_le_succ_ltP _ nB).
move: (nth_set1 pa nek).
set I := intersection (K -s S); move => [sa sb].
have /setCId_Pl di: disjoint (singleton I) S.
  by apply: disjoint_pr => u /set1_P -> eis; case/setC_P: sa => _.
move: (erefl x); rewrite {1} /x /nth_elt /nth_elts (induction_terms _ _ nB).
rewrite -/(nth_elts K n) /nth_more -/S -/I setCU2_l setC_v set0_U2 di setU_1.
by move => <-; split; fprops; move => y ys; apply: sw.
Qed.

Lemma nth_set9 K n:
   inc n Bnat -> sub K Bnat -> n <c cardinal K ->
   inc (nth_elt K n) K.
Proof. by move => pa pb pc; move:(nth_set7 pa pb pc) => [/setC_P []]. Qed.

Lemma nth_set8 K n m:
   inc n Bnat -> sub K Bnat -> n <c cardinal K ->
   m <c n -> (nth_elt K m) <c (nth_elt K n).
Proof.
move => nB KB nk mn.
have mB:= (BS_lt_int mn nB).
move: (nth_set7 nB KB nk); move => [_ _ _ h1]; apply: h1.
move:(nth_set7 mB KB (card_lt_ltT mn nk)) => [_ ub _ _].
move /(card_le_succ_ltP _ mB): mn => le1.
exact:(nth_set_M nB le1).
Qed.

Definition nth_set_fct K := Lf (nth_elt K) (Bint (cardinal K)) K.

Lemma nth_set_fct_bf K (f := (nth_set_fct K)):
  sub K Bnat -> finite_set K ->
  (bijection (nth_set_fct K) /\
  forall i j, inc i (source f) -> inc j (source f) -> i <c j ->
       Vf f i <c Vf f j).
Proof.
move => KB /BnatP kB.
have ax: lf_axiom (nth_elt K) (Bint (cardinal K)) K.
  move => n /(BintP kB) nk.
  by move:(nth_set7 (BS_lt_int nk kB) KB nk) => [/setC_P [h _] _ _ _].
have sf: source f = (Bint (cardinal K)) by rewrite /f/nth_set_fct;aw.
have pa: forall i j, inc i (source f) -> inc j (source f) -> i <c j ->
       Vf f i <c Vf f j.
  rewrite /f/nth_set_fct;aw;move => i j isf jsf; aw.
  move/(BintP kB): jsf => jk.
  by apply:nth_set8 => //; apply:(BS_lt_int jk kB).
split; last by exact.
rewrite sf in pa.
have fi: injection f.
  apply: lf_injective => // u v usf vsf sv.
  case: (Bnat_to_ell (Bint_S1 usf) (Bint_S1 vsf)) => cp //.
    by move: (proj2 (pa _ _ usf vsf cp)); rewrite /f/nth_set_fct;aw; case.
    by move: (proj2 (pa _ _ vsf usf cp)); rewrite /f/nth_set_fct;aw; case.
apply: bijective_if_same_finite_c_inj => //;rewrite /nth_set_fct; aw.
  by rewrite (card_Bint kB).
apply:finite_Bint.
Qed.

Lemma nth_set_10 K a: sub K Bnat -> finite_set K -> inc a K ->
  exists2 n, n <c (cardinal K) & a = (nth_elt K n).
Proof.
move => ha hb aK; move:( nth_set_fct_bf ha hb) => [[_ [ff fs]] _].
have hc: inc (cardinal K) Bnat by apply/BnatP.
have ax:lf_axiom (nth_elt K) (Bint (cardinal K)) K.
  move => t /(BintP hc) ta; apply:(nth_set9 _ ha ta).
  exact:(BS_lt_int ta hc).
move:fs; rewrite /nth_set_fct; aw => fs; move:(fs _ aK) => [x xa].
by aw => <-; exists x => //; apply/(BintP hc).
Qed.

permutations

Definition perm_int n := (permutations (Bint n)).

Lemma perm_intP f n: inc f (perm_int n) <->
   [/\ bijection f, source f = (Bint n) &
       target f = (Bint n)].
Proof.
split.
  by move/Zo_P => [/fun_set_P [ff sf tf] bf];split.
move => [pa pb pc]; apply:Zo_i => //; apply /fun_set_P; split=> //; fct_tac.
Qed.

Lemma perm_int_id n: inc (identity (Bint n)) (perm_int n).
Proof.
apply/perm_intP.
move:(identity_prop (Bint n)) => [_ pa pb].
split => //; apply: identity_fb.
Qed.

Lemma perm_int_inj n f: inc n Bnat -> inc f (perm_int n) ->
    (forall x y, x <c n -> y <c n -> Vf f x = Vf f y -> x = y).
Proof.
move => nB /perm_intP[ [[_ H] _] sf _].
rewrite sf in H.
by move => x y /(BintP nB) xs /(BintP nB) ys sv; apply:H.
Qed.

Lemma perm_int_surj n f: inc n Bnat -> inc f (perm_int n) ->
   forall y, y <c n -> exists2 x, x<c n & Vf f x = y.
Proof.
move => nB /perm_intP[ [_ [_ H]] sf tf].
rewrite sf tf in H.
by move => y /(BintP nB) /H [x /(BintP nB) sa sb]; exists x.
Qed.

Lemma perm_int_comp n f g:
    inc f (perm_int n) -> inc g (perm_int n) ->
    inc (f \co g) (perm_int n).
Proof.
move /perm_intP => [sa sb sc]/perm_intP [sa' sb' sc'].
apply/perm_intP; split;aw;apply: compose_fb => //.
by split; [fct_tac | fct_tac | rewrite sb sc'].
Qed.

Lemma perm_int_inv n f: inc f (perm_int n) ->
  inc (inverse_fun f) (perm_int n).
Proof.
move /perm_intP => [sa sb sc]; apply /perm_intP; split ; aw.
by apply: inverse_bij_fb.
Qed.

Lemma transposition_prop n i j
   (f:=Lf (fun z => Yo (z = i) j (Yo (z = j) i z)) (Bint n) (Bint n)):
   inc n Bnat -> inc i (Bint n) -> inc j (Bint n) ->
   [/\ inc f (perm_int n), Vf f i = j, Vf f j = i,
     forall k, inc k (Bint n) -> k <> i -> k <> j -> (Vf f k) = k &
     forall k, inc k (Bint n) -> Vf f (Vf f k) = k].
Proof.
move => nB iE jE.
set F := fun z => Yo (z = i) j (Yo (z = j) i z).
have la: lf_axiom F (Bint n) (Bint n).
   rewrite /F => z; Ytac h1; [ ue | Ytac h2; [ ue | done]].
have pa: Vf f i = j by rewrite /f; aw; Ytac0.
have pb: Vf f j = i by rewrite /f; aw; Ytac h1 => //; Ytac0.
have pc: forall k, inc k (Bint n) -> k <> i -> k <> j -> Vf f k = k.
  by move => k kE ki kj; rewrite /f; aw; Ytac0; Ytac0.
have pd:forall k, inc k (Bint n) -> Vf f (Vf f k) = k.
  move => k kE; case (equal_or_not k i) => ki; first by rewrite ki pa pb.
  case (equal_or_not k j) => kj; first by rewrite kj pb pa.
  by rewrite !(pc _ kE ki kj).
have sf: source f = (Bint n) by rewrite /f;aw.
have tf: target f = (Bint n) by rewrite /f;aw.
have ff: function f by apply: (lf_function la).
have bf: bijection f.
  split; split => //; first by rewrite sf => u v /pd {2} <- /pd {2} <- ->.
  rewrite sf tf => y ye;exists (Vf f y); [ Wtac | by rewrite pd].
split => //; apply /perm_intP; split => //.
Qed.

Lemma permutation_exists1 n i: inc n Bnat -> i <cn ->
    exists2 f, inc f (perm_int n) & Vf f \0c = i.
Proof.
move => nB lin.
move /(BintP nB): (card_le_ltT (czero_least (proj31_1 lin)) lin) => oE.
move /(BintP nB):lin => iI.
move:(transposition_prop nB iI oE) => [pa _ pb _ _].
move: pa pb;set f := Lf _ _ _ => pa pb; ex_tac.
Qed.

Lemma permutation_exists2 E n: inc n Bnat -> sub E (Bint n) ->
   exists2 f, inc f (perm_int n) & E = image_by_fun f (Bint (cardinal E)).
Proof.
move => nB;move:n nB E; apply: cardinal_c_induction.
  move => E; rewrite Bint_co00 => /sub_set0 ->.
  rewrite cardinal_set0 Bint_co00.
  by have h := (perm_int_id \0c); ex_tac; rewrite fun_image_set0.
move => n nB Hrec E seI.
case: (equal_or_not E (Bint (succ n))) => Ev.
  rewrite Ev (card_Bint (BS_succ nB)).
  set F := Bint (succ n).
  have bi:= (identity_fb F).
  exists (identity F). apply: perm_int_id.
  have {3} <-: source (identity F) = F by apply: identity_s.
  by rewrite -/(image_of_fun _) (surjective_pr0 (proj2 bi)) identity_t.
move: (setC_ne (conj seI Ev)) => [k1 /setC_P [k1I k1E]].
move:(Bint_pr4 nB) =>[].
set In:= Bint n; set Im := (Bint (succ n)) => sa sb.
have Inm: forall i, inc i In -> (inc i Im /\ i <> n).
  by move => i ein; rewrite - sa; split; [ fprops | dneg w; ue].
have nIm: inc n Im by exact : (Bint_si nB).
set k0:= Yo (inc n E) k1 n.
have kI: inc k0 Im by rewrite /k0; Ytac h.
have kE: ~(inc k0 E) by rewrite /k0; Ytac h.
set F := (E +s1 k0) -s1 n.
have eq0: F +s1 n = E +s1 k0.
  rewrite /k0;set_extens t; case/setU1_P.
  + by move/setC1_P => [].
  + move => ->; Ytac h; fprops.
  + move => tE; case (equal_or_not t n) => etn; first by rewrite etn; fprops.
    apply /setU1_P; left; apply/setC1_P; split ; fprops.
  + rewrite /F/k0;move => ->;Ytac h; fprops; case (equal_or_not k1 n).
      by move ->; fprops.
    move => h'; apply/setU1_P; left; apply/setC1_P; fprops.
have fIn: sub F In.
  move => t /setC1_P [ta tb].
  have: inc t Im by case /setU1_P:ta; [apply: seI | move => ->].
  rewrite - sa; case /setU1_P => //.
move: (Hrec _ fIn) => [f /Zo_P [/fun_set_P[ff sf tf] fb] fv].
rewrite -/In in sf tf.
pose g i := Yo (i = n) k0 (Yo (Vf f i = k0) n (Vf f i)).
have pa: lf_axiom g Im Im.
  hnf; rewrite/g - {1} sa; move => t;case /setU1_P; last by move => ->; Ytac0.
  move => ti;Ytac h => //; Ytac h' => //; rewrite - sa; apply/setU1_r;Wtac.
have sg:surjection (Lf g Im Im).
  apply: lf_surjective => // y; rewrite - {1} sa /g; case /setU1_P.
    case: (equal_or_not y k0) => yk0; first by exists n => //; Ytac0.
    rewrite - tf => /(proj2 (proj2 fb)) [x xsf fx].
    rewrite sf in xsf; move: (Inm _ xsf) => [xa xb]; ex_tac.
    by rewrite fx; Ytac0; Ytac0.
  move => ->;move: (kI) ; rewrite -/Im - {1} sa; case /setU1_P.
    rewrite - tf; move/(proj2 (proj2 fb)) => [x xsf fx].
    rewrite sf in xsf; move: (Inm _ xsf) =>[xa xb]; ex_tac.
    by rewrite /g; Ytac0; Ytac0.
  by move => kn;exists k0 => //;rewrite /g; Ytac0.
set G:= (Lf g Im Im).
have bg:bijection (Lf g Im Im).
  have cc: cardinal (source G) = cardinal (target G) by rewrite/ G; aw.
  have fsg: finite_set (source G).
    by rewrite /G /Im; aw; apply:finite_Bint.
   exact:(bijective_if_same_finite_c_surj cc fsg sg).
have gP: inc G (permutations Im).
  apply: Zo_i => //; apply/fun_set_P; rewrite /G;split;aw; fct_tac.
have nf: ~ (inc n F) by move/setC1_P => [].
have nk0: ~ inc k0 E by rewrite /k0; Ytac h.
move: (f_equal cardinal eq0).
rewrite (card_succ_pr nf)(card_succ_pr nk0).
move/(succ_injective1 (CS_cardinal F)(CS_cardinal E)) => <-.
move:(sub_smaller fIn); rewrite /In (card_Bint nB) => le1.
move:(Bint_M nB); rewrite -/In -/Im => sub2.
move: fv (Bint_M1 nB le1).
set Ik:= (Bint (cardinal F)); rewrite -/In => fv sub1.
move: (sub_trans sub1 sub2) => sub3.
have fG: function G by fct_tac.
have ssG: sub Ik (source G) by rewrite /G; aw.
have ssF: sub Ik (source f) by rewrite sf.
ex_tac.
set_extens t.
  move => tE;case (equal_or_not t n) => etn.
    move:(setU1_1 k0 E); rewrite - eq0 => /setU1_P; case.
      rewrite fv; move => /(Vf_image_P ff ssF) [u ua ub].
      apply/(Vf_image_P fG ssG); ex_tac;rewrite /G; aw; last by apply:sub3.
      rewrite /g;Ytac h1; first by move: (sub1 _ ua); rewrite h1.
      by rewrite - ub; Ytac0.
    by move => w; case kE; rewrite w - etn.
  move: (setU1_r k0 tE); rewrite - eq0 => /setU1_P;case => //.
  rewrite fv; move => /(Vf_image_P ff ssF) [u ua ub].
  apply/(Vf_image_P fG ssG); ex_tac;rewrite /G; aw; last by apply:sub3.
  rewrite /g;Ytac h1; first by move: (sub1 _ ua); rewrite h1.
  by rewrite - ub; Ytac h=> //; case kE; rewrite - h.
move /(Vf_image_P fG ssG) => [u uik ->]; move:(sub3 _ uik)=> uIm.
rewrite /G; aw;rewrite /g; Ytac un.
   by case sb; rewrite -un; exact:(sub1 _ uik).
have: inc (Vf f u) F by rewrite fv; apply/(Vf_image_P ff ssF); ex_tac.
move/setC1_P => [ha hb];Ytac h1; first by move: h1; rewrite /k0;Ytac h2.
by case/setU1_P: ha.
Qed.

Number of decompositions

Definition nds_sc n X g := osum_expansion (fun z => (X (Vf g z))) n.

Definition nds_sums n X := fun_image (perm_int n) (nds_sc n X).

Definition nds_card n X := cardinal (nds_sums n X).

Definition nds_ax X n:= ord_below_n X n.

Lemma nds_a n X: inc n Bnat -> nds_card n X <=c (factorial n).
Proof.
move=> nB.
rewrite /nds_card/nds_sums.
set a := (perm_int n).
set b := fun_image _ _.
set E:= (Bint n).
have cE: cardinal E = n by apply card_Bint.
have fsE: finite_set E by red; rewrite cE; apply /BnatP.
move: (number_of_permutations fsE); rewrite cE; move => <-.
apply: surjective_cardinal_le.
  exists (Lf (nds_sc n X) a b); red; aw; split => //.
apply:lf_surjective.
   move=> t ta; apply /funI_P; ex_tac.
by move=> y /funI_P.
Qed.

Lemma nds_b X n f: inc n Bnat -> nds_ax X n->
   inc f (perm_int n) ->
   (nds_ax (fun z => X (Vf f z)) n /\ ordinalp (nds_sc n X f)).
Proof.
move=> nB ax => /Zo_P [] /fun_set_P [ff sf tf] bf.
suff pc: nds_ax (fun z : Set => X (Vf f z)) n.
  by split => //; apply: OS_osum_expansion.
move => t tn; apply: ax; apply/(BintP nB); Wtac.
by rewrite sf; apply/(BintP nB).
Qed.

Lemma nds_sc_exten X X' n f:
  inc n Bnat -> (same_below X X' n) ->
  inc f (perm_int n) ->
  nds_sc n X f = nds_sc n X' f.
Proof.
move =>nB h /Zo_P [] /fun_set_P [fg sg tg] bg;apply: (osum_expansion_exten nB).
move => i /(BintP nB) ia; apply: h; apply/(BintP nB); Wtac.
Qed.

Lemma nds_m n X g (Y:= fun z => X (Vf g z)):
  inc n Bnat -> nds_ax X n -> inc g (perm_int n) ->
  nds_card n X = nds_card n Y.
Proof.
move => nB ax /Zo_P [] /fun_set_P [fg sg tg] bg.
rewrite /nds_card /nds_sums; apply: f_equal.
set E := perm_int n.
set_extens t; move /funI_P => [z ze ->]; apply /funI_P.
  move: (inverse_bij_fb bg) => ibg.
  move: ze => /Zo_P [] /fun_set_P [fz sz tz] bz.
  have fa: (inverse_fun g) \coP z by red;aw;split => //; [fct_tac | ue].
  have fb: function ((inverse_fun g) \co z) by fct_tac.
  exists ((inverse_fun g) \co z).
  apply: Zo_i; [ apply /fun_set_P;red;aw;split => // | by apply compose_fb ].
  apply:(osum_expansion_exten nB) => i lin.
  have iz: inc i (source z) by rewrite sz; apply /(BintP nB i).
  have cp: inverse_fun g \coP z by split; [ fct_tac | exact | aw; ue].
  have fzy: inc (Vf z i) (target g) by rewrite tg - tz; Wtac.
  by rewrite /Y (compf_V cp iz) (inverse_V bg fzy).
move: ze => /Zo_P [] /fun_set_P [fz sz tz] bz.
have fa: g \coP z by red;aw;split => //; ue.
have fb: function (g \co z) by fct_tac.
exists (g \co z).
  apply: Zo_i; [ apply /fun_set_P;red;aw;split => // | by apply compose_fb ].
apply:(osum_expansion_exten nB) => i lin.
by rewrite /Y compf_V // sz; apply/(BintP nB i).
Qed.

Lemma nds_c n X: inc n Bnat ->
   (\1c <=c nds_card n X /\ inc (nds_card n X) Bnat).
Proof.
move=> nB; move: (nds_a X nB) => pa.
move:(BS_le_int pa (BS_factorial nB)) => pb.
split => //.
rewrite /nds_card/nds_sums; apply: card_ge1; first by fprops.
apply: cardinal_nonemptyset1; apply:funI_setne.
exists (identity (Bint n)).
apply: Zo_i; [ apply /fun_set_P;red;aw;split;fprops | apply identity_fb].
Qed.

Lemma nds_d X n: (n = \0c \/ n = \1c) ->
  nds_ax X n -> nds_card n X = \1c.
Proof.
move=> np ax.
have nB: inc n Bnat by case: np => ->; fprops.
apply: card_leA.
  by move: (nds_a X nB); case: np => ->; rewrite ? factorial0 ? factorial1.
exact (proj1 (nds_c X nB)).
Qed.

Lemma nds_e X: nds_ax X \2c -> osum_expansion X \2c = (X \1c) +o (X \0c).
Proof.
rewrite - succ_one => pa.
rewrite (osum_expansion_succ _ BS1) (osum_expansion1) //; apply: pa.
rewrite succ_one; apply: card_lt_02.
Qed.

Lemma nds_f n X (f := identity (Bint n)) :
  inc n Bnat -> nds_ax X n ->
  (inc f (perm_int n) /\ (nds_sc n X f = osum_expansion X n)).
Proof.
move=> nB ax.
have bi: bijection f by apply identity_fb.
split.
  by rewrite /f; apply: Zo_i => //; apply /fun_set_P; red;aw;split;fprops.
apply:(osum_expansion_exten nB) => i lin.
by rewrite /f identity_V // ; apply/(BintP nB).
Qed.

Lemma nds_g (X:=(variant \0c \1o omega0)):
    nds_ax X \2c /\ nds_card \2c X = \2c.
Proof.
move: osum2_nc => /= nc.
have nX: nds_ax X \2c by move => t t2; rewrite /X /variant; Ytac h; fprops.
split => //; apply: card_leA.
  by move: (nds_a X BS2); rewrite factorial2.
move: (nds_f BS2 nX) => [ha hb].
have ne: \1c <> \0c by fprops.
apply /card_le2P.
exists (\1o +o omega0), (omega0 +o \1o); split => //;apply /funI_P; last first.
  exists (identity (Bint \2c)) => //.
  by rewrite hb (nds_e nX) /X /variant; Ytac0; Ytac0.
set I:= (Bint \2c).
have I1: inc \1c I by apply/(BintP BS2); apply: card_lt_12.
have I0: inc \0c I by apply/(BintP BS2); apply: card_lt_02.
have iv: forall y, inc y (Bint \2c) -> y = \0c \/ y = \1c.
    by move=> y /(BintP BS2) => h; apply card_lt2.
have ta: lf_axiom (variant \0c \1c \0c) I I.
  by move => t _; rewrite /variant; Ytac h.
have fp: inc (Lf (variant \0c \1c \0c) I I) (permutations I).
  apply/Zo_i; first by apply /fun_set_P; split; [apply: lf_function | aw | aw].
  apply: lf_bijective => //.
    move=> u v us vs.
    rewrite /variant; case: (iv _ us); case: (iv _ vs);
       move => -> ->; Ytac0 => //; Ytac0 => //.
    move => y yv; case: (iv _ yv); move => ->.
      by exists \1c => //; rewrite /variant; Ytac0.
      by exists \0c => //; rewrite /variant; Ytac0.
have ax2:= (proj1 (nds_b BS2 nX fp)).
exists (Lf (variant \0c \1c \0c) I I); first exact.
by rewrite /nds_sc nds_e; aw; aw; rewrite /X /variant; repeat Ytac0.
Qed.

Lemma nds_h (A:= omega0 ^o \2o) (B:= omega0) (C := omega0 +o \1o)
  (s1 := A +o (B +o C)) (s2:= A +o (C +o B)) (s3 := B +o (A +o C))
  (s4 := B +o (C +o A)) (s5:= C +o (A +o B)) (s6 := C +o (B +o A)):
  cardinal (((doubleton s1 s2) \cup (doubleton s3 s5)) \cup
    (doubleton s4 s6)) = card_five.
Proof.
set T := union2 _ _.
move: OS_omega OS1 OS2 => oB o1 o2.
have oA: ordinalp A by apply: OS_pow.
have oC: ordinalp C by apply: OS_sum2.
move: (ord_negl_p4 ord_lt_02); rewrite opowx0 -/A => pa.
move: (ord_negl_p4 ord_lt_12); rewrite (opowx1 oB) -/A -/B => pb.
have e1: s3 = A +o C by rewrite /s3 (osumA oB oA oC) pb.
have e2: s6 = C +o A by rewrite /s6 pb.
have pc: C +o A = A by rewrite - (osumA oB OS1 oA) pa pb.
have pd: (doubleton s4 s6) = singleton A by rewrite /s4 e2 pc pb.
have e3: s2= A +o (B +o B).
   by rewrite /s2 - (osumA oB o1 oB) (osum_int_omega ord_lt_1omega).
have e4: s5= A +o B by rewrite /s5 (osumA oC oA oB) pc.
set T1:= (union2 (doubleton s1 s2) (doubleton s3 s5)).
have bz: B <> \0o by apply: omega_nz.
have onz: \1o <> \0o by fprops.
case: (equal_or_not C \0o) => cz; first by move: (osum2_zero oB OS1 cz) => [_].
have nAt: ~ (inc A T1).
  have sA: forall b, ordinalp b ->A = A +o b -> b = \0o.
     move => b ob h; symmetry in h; exact (osum_a_ab oA ob h).
  case /setU2_P; case /set2_P.
  - by move/(sA _ (OS_sum2 oB oC)) => /(osum2_zero oB oC) [_].
  - by move/(sA _ (OS_sum2 oC oB)) => /(osum2_zero oC oB) [].
  - by rewrite e1; move /(sA _ oC).
  - by rewrite e4; move /(sA _ oB).
have ->: T = T1 +s1 A by rewrite -pd //.
rewrite /card_five (card_succ_pr nAt); congr succ.
set T2 := (doubleton s1 s2) +s1 s3.
have ->: T1 = T2 +s1 s5.
  set_extens t.
     case /setU2_P => h; first by apply /setU1_P; left; apply /setU1_P; left.
     case /set2_P :h => h; first by apply /setU1_P; left; apply /setU1_P; right.
     by apply /setU1_P; right.
  case /setU1_P =>h; last by apply /setU2_P; right; apply/set2_P; right.
  case /setU1_P:h => h; last by apply /setU2_P; right; apply/set2_P; left.
  by apply /setU2_P; left.
have aux: forall b c, ordinalp b -> ordinalp c -> A +o b = A +o c -> b = c.
  move => b c ob oc ; apply: (osum2_simpl ob oc oA).
have auB: forall b c, ordinalp b -> ordinalp c -> B +o b = B +o c -> b = c.
  move => b c ob oc ; apply: (osum2_simpl ob oc oB).
case (equal_or_not B C) => nCB; first by move: (osum_a_ab oB o1 (esym nCB)).
have nat2: ~ inc s5 T2.
  rewrite /T2 e4 /s1 e1 e3 => /setU1_P; case => h; last first.
    case: nCB; exact (aux _ _ oB oC h).
  case /set2_P:h=> h.
       move: (aux _ _ oB (OS_sum2 oB oC) h) => h1; symmetry in h1.
       case: cz; exact: (osum_a_ab oB oC h1).
     move: (aux _ _ oB (OS_sum2 oB oB) h) => h1; symmetry in h1.
     case: bz; exact: (osum_a_ab oB oB h1).
move: (ord_lt_1omega) => [h2 h3].
move: (ord_succ_lt oB) => h4.
have nat3: ~ inc s3 (doubleton s1 s2).
  rewrite /s1 e1 e3;case /set2_P=> h.
    move: (aux _ _ oC (OS_sum2 oB oC) h) => h1.
    move: (ord_le_ltT h2 h4) => [_ h5].
    by move: (auB _ _ o1 oC h1); rewrite /C (ord_succ_pr oB).
  move: (aux _ _ oC (OS_sum2 oB oB) h) => h1.
  case: h3; exact: (auB _ _ o1 oB h1).
rewrite /card_four (card_succ_pr nat2); apply: f_equal.
rewrite /card_three (card_succ_pr nat3); apply: f_equal.
apply: cardinal_set2.
rewrite /s1 e3 => h; move: (aux _ _ (OS_sum2 oB oC) (OS_sum2 oB oB) h) => h1.
by case: nCB; rewrite (auB _ _ oC oB h1).
Qed.

Definition nds_F n :=
 \osup (Zo Bnat (fun z => exists2 X, nds_ax X n & nds_card n X = z)).

Lemma Bnat_sup_pr T (s:= \osup T) k:
  sub T Bnat -> inc k Bnat -> (forall i, inc i T -> i <=c k) ->
  [/\ inc s Bnat, s <=c k,
    (forall i, inc i T -> i <=c s) &
    (T = emptyset \/ inc s T)].
Proof.
move=> TB kB km.
have qa: forall t, inc t Bnat -> ordinalp t.
   move => t tb; apply: OS_cardinal; fprops.
move: (qa _ kB) => ok.
have pa: ordinal_set T by move=> t tT; apply: qa; apply: TB.
have pb: s <=o k.
  apply: ord_ub_sup => // i iT; move: (km _ iT); apply: ordinal_cardinal_le.
have pc: inc s Bnat.
  move: kB => /(ord_ltP OS_omega) => ko; apply /(ord_ltP OS_omega).
  ord_tac.
have pd: s <=c k by apply: ordinal_cardinal_le3; fprops.
split => //.
  move=> i iT.
  have: i <=o s by apply:ord_sup_ub => //.
  by apply: ordinal_cardinal_le3; fprops.
case: (emptyset_dichot T) => tne; first by left.
case: (ord_sup_inVlimit pa tne); first by right.
move => li; move: (omega_limit2 li) => [_ _ li2].
case: (ordinal_irreflexive (qa _ pc) (li2 _ pc)).
Qed.

Lemma nds_j n (f := nds_F n): inc n Bnat ->
  [/\ inc f Bnat,
   f <=c factorial n,
   (exists2 X, nds_ax X n & nds_card n X = f) &
   (forall X, nds_ax X n -> nds_card n X <=c f)].
Proof.
move => nB.
set T := (Zo Bnat(fun z => exists2 X, nds_ax X n & nds_card n X = z)).
have ta: sub T Bnat by apply: Zo_S.
move: (BS_factorial nB) => tb.
have tc: (forall i, inc i T -> i <=c (factorial n)).
  rewrite /T;move=> i /Zo_P [iB [X ea <-]]; exact: (nds_a X nB).
move: (Bnat_sup_pr ta tb tc) => [pa pb pc pd].
have pe: forall X, nds_ax X n -> inc (nds_card n X) Bnat.
  move=> X ax; move: (nds_a X nB) => le1; apply: (BS_le_int le1 tb).
have pf: forall X, nds_ax X n -> nds_card n X <=c f.
  by move=> X xv; apply: pc; apply: Zo_i;fprops; exists X.
case: pd => h; last by move:h => /Zo_P [_].
set X := (fun z: Set => \0o).
have aX: nds_ax X n by rewrite /X;move => i _ /=; fprops.
by empty_tac1 (nds_card n X); apply: Zo_i; [by apply: pe | exists X].
Qed.

Lemma nds_k: (nds_F \0c = \1c /\ nds_F \1c = \1c).
Proof.
move: nds_d => h.
move: (nds_j BS0); set f := nds_F \0c;move => [_ _ p3 _].
move: p3 => [X ax <-].
move: (nds_j BS1); set g := nds_F \0c;move => [_ _ p2 _].
move: p2 => [Y ay <-].
have pa: \0c = \0c \/ \0c = \1c by left.
have pb: \1c = \0c \/ \1c = \1c by right.
by rewrite (h X _ pa ax) (h Y _ pb ay).
Qed.

Lemma nds_l: nds_F \2c = \2c.
Proof.
move: (nds_j BS2); set f := nds_F \2c.
move => [p1 p2 p3 p4].
move: nds_g => [ax xv]; move: (p4 _ ax); rewrite xv => le1.
rewrite factorial2 in p2; co_tac.
Qed.

Lemma nds_n e c1 c2 r1 r2:
  ordinalp e -> ordinalp c1 -> r1 <o omega0 ^o e ->
  \0o <o c2 -> ordinalp r2 ->
  (omega0 ^o e *o c1 +o r1) +o (omega0 ^o e *o c2 +o r2) =
  (omega0 ^o e *o (c1 +o c2) +o r2).
Proof.
set p := omega0 ^o e;move => oe oc1 pa pb or2.
have op := OS_pow OS_omega oe.
have or1:= (proj31_1 pa).
have oc2:= (proj32_1 pb).
have oa := OS_prod2 op oc1.
have ob := OS_prod2 op oc2.
have oc := OS_sum2 ob or2.
move:(ord_negl_prod or1 op pb (indecomp_prop1 (indecomp_prop4 oe) pa)) => H.
rewrite - (osumA oa or1 oc) (osumA or1 ob or2) H (osumA oa ob or2).
by rewrite - (osum_prodD oc1 oc2 op).
Qed.

Lemma nds_o e (c r: fterm) n:
  inc n Bnat -> ordinalp e ->
  (forall i, i<=c n -> \0o <o c i /\ r i <o omega0 ^o e) ->
  osum_expansion (fun i => omega0 ^o e *o (c i) +o r i) (succ n) =
  omega0 ^o e *o (osum_expansion c (succ n)) +o (r \0c).
Proof.
move => nb oe; move: (OS_pow OS_omega oe) => op.
move: n nb; apply: cardinal_c_induction.
  move => H; rewrite succ_zero.
  move: (H _ (czero_least CS0)) => [[[_ oc _] _] [[or _ _] _]].
  have ot:= (OS_sum2 (OS_prod2 op oc) or).
  by rewrite (osum_expansion1) // (osum_expansion1 oc).
move => n nB Hrec ol.
have sa: forall i, i <=c n -> \0o <o c i /\ r i <o omega0 ^o e.
  move:(card_le_succ nB) => nn i lein; apply: ol;co_tac.
move: (ol _ (card_leR (CS_succ n))) => [/proj32_1 ocn rs].
have or0:=(proj31_1 (proj2 (ol _ (czero_least (CS_succ n))))).
rewrite (osum_expansion_succ _ (BS_succ nB)) (Hrec sa).
have pc: \0o <o osum_expansion c (succ n).
  have: ord_below_n c n.
    move => i lin; exact : (proj32_1 (proj1 (sa i (proj1 lin)))).
  move /(OS_osum_expansion nB) => ha.
  have [[_ oc0 _] /nesym cnz]:= proj1 (ol _ (card_le_succ nB)).
  rewrite (osum_expansion_succ _ nB).
  by apply:(ord_ne0_pos (OS_sum2 oc0 ha)) => /(osum2_zero oc0 ha) [].
by rewrite (nds_n oe ocn rs pc or0) (osum_expansion_succ _ (BS_succ nB)).
Qed.

Lemma nds_p1 e (c r: fterm) n f (X := (fun i => omega0 ^o e *o (c i) +o r i)):
  inc n Bnat -> ordinalp e ->
  (forall i, i<=c n -> \0o <o c i /\ r i <o omega0 ^o e) ->
  (forall i, i<=c n -> c i <o omega0) ->
  inc f (perm_int (succ n)) ->
  nds_sc (succ n) X f =
  omega0 ^o e *o (osum_expansion c (succ n)) +o (r (Vf f \0c)).
Proof.
move => nB oe h1 h2 fp.
have aux: forall n Z, inc n Bnat -> (forall i, i <c n -> inc (Z i) Bnat)
  -> osum_expansion Z n = card_sumb (Bint n) Z.
  move => m z mb; move: m mb; apply: cardinal_c_induction.
    move => _; rewrite osum_expansion0 /card_sumb csum_trivial //.
    bw;exact:Bint_co00.
  move => m mB Hrec zp; rewrite (osum_expansion_succ _ mB).
  move: (Bint_pr4 mB) => [<- sb].
  have ha: forall i, i <c m -> inc (z i) Bnat.
    move => i lim; apply: zp; move: (card_lt_succ mB) => hb; co_tac.
  have zmB:= (zp _ (card_lt_succ mB)).
  have sB: inc (card_sumb (Bint m) z) Bnat.
    apply:finite_sum_finite; split.
      by hnf; bw;move => i lim; bw; apply: ha; apply /(BintP mB).
    bw; apply:finite_Bint.
  by rewrite (csumA_setU1 z sb) (Hrec ha) csumC (osum2_2int zmB sB).
move:(fp) => /Zo_P [] /fun_set_P [fz sz tz] bz.
have sa: forall i, i <=c n -> \0o <o c (Vf f i) /\ r (Vf f i) <o omega0 ^o e.
  move => i /(BintsP nB) lin; apply: h1; apply /(BintsP nB); Wtac.
transitivity
 (osum_expansion (fun i => omega0 ^o e *o (c (Vf f i)) +o r (Vf f i)) (succ n)).
  by apply:(osum_expansion_exten (BS_succ nB)) => i lin.
have h3: forall i,i <c (succ n) -> inc (c i) Bnat.
  by move => i /(card_lt_succ_leP nB) /h2 /olt_omegaP.
have h4: forall i,i <c (succ n) -> inc (c (Vf f i)) Bnat.
  move => i /(BintP (BS_succ nB)) lin; apply: h3.
  apply /(BintP (BS_succ nB)); Wtac.
rewrite (nds_o nB oe sa) (aux _ _ (BS_succ nB) h3) (aux _ _ (BS_succ nB) h4).
rewrite - {1} sz - tz (csum_Cn' c bz); reflexivity.
Qed.

Lemma the_CNF_omega_k k (X := omega0 +o k)
  (r:= fun i => CNFbvo (Vg (P (Q (the_CNF X))))
        (Vg (Q (Q (the_CNF X)))) (cpred (P (the_CNF X)))):
  inc k Bnat ->
  [/\ \0o <o X , the_CNF_degree X = \1o & r \0c = k].
Proof.
move => /olt_omegaP ko.
have ok: ordinalp k by ord_tac.
have ox: ordinalp X by apply: (OS_sum2 OS_omega ok).
have xp: \0o <o X.
  apply: ord_ne0_pos => // sz.
  by move: (osum2_zero OS_omega ok sz) => [p1 _]; move: omega_nz.
case : (ord_zero_dichot ok) => kz.
   set e := fun i: Set => \1o.
   have ax: CNFb_axo e e \1c.
    split; first split.
    + apply: ord_le_2omega.
    + move => i lin; rewrite /e; fprops.
    + move => i lin; rewrite /e; apply:ord_lt_1omega.
    + by move => i iB /card_lt1 h; case: (@succ_nz i).
    + move => i lin; rewrite /e; apply: ord_lt_01.
  move: (CNFbB_prop ax BS1); set y := (CNFbB \1c e e); move => [ax2 yv].
  have py2: P y = \1c by rewrite /y /CNFbB; aw.
  move: (CNFB_ax_simp ax2) => [_ ax4].
  move: BS0 card_lt_01 => b0 lt01.
  have eq1: X = CNFBv y.
    rewrite py2 in ax4.
    rewrite /X kz (osum0r OS_omega) /CNFBv py2 /CNFbvo.
    rewrite (CNFq_p3 (proj1 ax4) lt01) /cantor_mon.
    rewrite /y /CNFbB !(pr1_pair, pr2_pair) /e; bw; Ytac0.
    by rewrite (opowx1 OS_omega) (oprod1r OS_omega).
  move:(the_CNF_p0 ox) => [sa sb].
  rewrite - sb in eq1; rewrite py2 in ax4.
  rewrite /r /the_CNF_degree.
  rewrite (CNFB_unique sa ax2 eq1) py2 - succ_zero (cpred_pr1 CS0).
  split;[ by exact | by rewrite /y /CNFbB; aw; bw; Ytac0 |].
  by rewrite /CNFbvo (CNFq_p2).
pose e i := Yo (i = \0c) \0o \1o.
pose c i := Yo (i = \0c) k \1o.
move:card1_nz => H.
move: card_lt_12 => lt12.
move: card_lt_02 => lt02.
move: ord_lt_01 BS0 BS1 => l01 bs0 bs1.
have e0: e \0c = \0o by rewrite /e; Ytac0.
have e1: e \1c = \1o by rewrite /e; Ytac0.
have c0: c \0c = k by rewrite /c; Ytac0.
have c1: c \1c = \1o by rewrite /c; Ytac0.
have ax: CNFb_axo e c \2c.
  split; first split.
  + apply: ord_le_2omega.
  + move => i lin; rewrite /e; Ytac h; fprops.
  + by move => i lin; rewrite /c; Ytac h => //; apply: ord_lt_1omega.
  + move => i iB /card_lt2; rewrite /e; move: (@succ_nz i) => ss.
    rewrite - succ_zero; case => // si.
    by move: (succ_injective1 (CS_Bnat iB) CS0 si) => iz;Ytac0; Ytac0.
  + move => i lin; rewrite /c; Ytac h => //.
move: (CNFbB_prop ax BS2); set y := (CNFbB \2c e c); move => [ax2 yv].
have py2: P y = \2c by rewrite /y /CNFbB; aw.
move: (CNFB_ax_simp ax2) => [_ ax4].
have eq1: X = CNFBv y.
  rewrite py2 in ax4.
  move: (CNFq_p7 (proj1 ax4) lt12).
  rewrite /X /CNFBv /y /CNFbB !(pr1_pair, pr2_pair) -/CNFbvo => ->.
  rewrite /cantor_mon; bw; repeat Ytac0; rewrite e0 c0 e1 c1.
  by rewrite opowx0 (opowx1 OS_omega) (oprod1r OS_omega) (oprod1l ok).
move:(the_CNF_p0 ox) => [sa sb].
rewrite - sb in eq1; rewrite py2 in ax4.
rewrite /r /the_CNF_degree.
rewrite (CNFB_unique sa ax2 eq1) py2 - succ_one (cpred_pr1 CS1).
split;[ by exact | by rewrite /y /CNFbB; aw; bw; Ytac0 |].
rewrite /CNFbvo (CNFq_p3 (proj1 ax4) lt02).
rewrite /cantor_mon /y /CNFbB; aw; bw; Ytac0; Ytac0.
by rewrite c0 e0 opowx0 (oprod1l ok).
Qed.

Lemma nds_q1 e X n
  (r:= fun i => CNFbvo (Vg (P (Q (the_CNF (X i)))))
        (Vg (Q (Q (the_CNF (X i)))))
       (cpred (P (the_CNF (X i)))))
  (F:= fun_image (Bint (succ n)) r):
  inc n Bnat ->
  (forall i, i<=c n -> \0o <o X i) ->
  (forall i, i<=c n -> the_CNF_degree (X i) = e) ->
  nds_card (succ n) X = cardinal F.
Proof.
move => nB pa pb.
have oe: ordinalp e.
  have ha:= (czero_least (CS_Bnat nB)).
  rewrite -(pb _ ha); exact: (OS_the_CNF_degree (proj32_1 (pa _ ha))).
pose c i := Vg (Q (Q (the_CNF (X i)))) (cpred (P (the_CNF (X i)))).
have pc: forall i, i<=c n -> [/\ \0o <o c i, c i <o omega0, r i <o omega0 ^o e
      & X i = omega0 ^o e *o (c i) +o (r i)].
  move => i lein; move: (pa _ lein) (pb _ lein) => sa sb.
  by move: (the_CNF_split sa); rewrite sb.
have pd: (forall i, i<=c n -> \0o <o c i /\ r i <o omega0 ^o e).
  by move => i /pc[].
have pe: (forall i, i<=c n -> c i <o omega0) by move => i /pc[].
rewrite /nds_card /nds_sums.
set E := (permutations (Bint (succ n))).
set s1:= omega0 ^o e *o (osum_expansion c (succ n)).
have os1: ordinalp s1.
  apply: (OS_prod2 (OS_pow OS_omega oe)).
  apply: (OS_osum_expansion (BS_succ nB)) => i /(card_lt_succ_leP nB) lin.
  by move:(pc _ lin) => [ /proj32_1 h _ _ _].
set F1 := (fun_image E (nds_sc (succ n) X)).
set F2 := (fun_image E (fun f => r (Vf f \0c))).
have pf: forall f, inc f E -> nds_sc (succ n) X f = s1 +o (r (Vf f \0c)).
  move => f fp; rewrite - (nds_p1 nB oe pd pe fp).
  by apply:(nds_sc_exten (BS_succ nB) _ fp) => i /(card_lt_succ_leP nB) /pc [].
have pg: forall z, inc z E -> inc (Vf z \0c) (Bint (succ n)).
  move => z /Zo_P [] /fun_set_P [fz sz tz] bz; Wtac.
  rewrite sz; apply/(BintsP nB); fprops.
have osF: ordinal_set F2.
  by move => s /funI_P [z /pg /(BintsP nB) /pc [_ _ /proj31_1 h _] ->].
have ->: cardinal F1 = cardinal F2.
  symmetry; apply/card_eqP; exists (Lf (fun z => s1 +o z) F2 F1).
  split; aw; apply:lf_bijective.
  + by move => s /funI_P [z ze -> ]; apply /funI_P; ex_tac; rewrite (pf _ ze).
  + by move => u v /osF ou /osF ov /(osum2_simpl ou ov os1).
  + move => s /funI_P [z ze -> ]; rewrite (pf _ ze).
    exists (r (Vf z \0c)) => //;apply/funI_P; ex_tac.
apply: f_equal; set_extens t.
  move => /funI_P [z /pg ze -> ]; apply /funI_P; ex_tac.
move => /funI_P [i /(BintP (BS_succ nB)) iI ->]; apply /funI_P.
move: (permutation_exists1 (BS_succ nB) iI) => [f fe <-]; ex_tac.
Qed.

Lemma nds_q2 e X n: inc n Bnat ->
  (forall i, i<=c n -> \0o <o X i) ->
  (forall i, i<=c n -> the_CNF_degree (X i) = e) ->
  nds_card (succ n) X <=c (succ n).
Proof.
move => pa pb pc. rewrite (nds_q1 pa pb pc).
set r := fun i:Set => _.
move: (fun_image_smaller (Bint (succ n)) r).
by rewrite (card_Bint (BS_succ pa)).
Qed.

Lemma nds_q3 n: inc n Bnat -> exists X,
  [/\ nds_ax X (succ n), forall i, i<c succ n -> \0o <o X i,
  (forall i, i<=c n -> the_CNF_degree (X i) = \1o) &
  nds_card (succ n) X = (succ n)].
Proof.
move=> nB.
pose X i := (omega0 +o i).
have Ha: (forall i, i <=c n -> \0o <o X i).
  move => i lein; move:(BS_le_int lein nB) => iB.
  exact:(proj31 (the_CNF_omega_k iB)).
have Hb:(forall i, i <=c n -> the_CNF_degree (X i) = \1o).
   move => i lein; move:(BS_le_int lein nB) => iB.
   exact:(proj32 (the_CNF_omega_k iB)).
have Hc:(forall i, i<c succ n -> \0o <o X i).
   by move => i/(card_lt_succ_leP nB) /Ha.
have Hd:nds_ax X (succ n) by move => i /Hc /proj32_1.
exists X; split => //.
rewrite (nds_q1 nB Ha Hb).
set E := (Bint (succ n)).
set F := fun_image _ _.
have ->: F = fun_image E id.
   by set_extens t => /funI_P [z ze ->]; apply/funI_P; ex_tac;
   rewrite (proj33 (the_CNF_omega_k (Bint_S1 ze))).
have ->: (fun_image E id) = E.
   set_extens t; first by move => /funI_P [z ze ->].
   move => te; apply/funI_P; ex_tac.
exact: (card_Bint (BS_succ nB)).
Qed.

Definition nds_type0 X n :=
  exists2 i, i<c n & X i = \0o.

Definition nds_type' X n k :=
  (forall i, i<c n -> \0o <o X i) /\
  (exists m, [/\ ordinalp m,
     (forall i, i<c n -> m <=o the_CNF_degree (X i)) &
     cardinal (Zo (Bint n)(fun i => the_CNF_degree (X i) = m)) =k]).

Definition nds_type X n k:=
   ((k = \0c) /\ (nds_type0 X n)) \/
   (k <> \0c /\ (nds_type' X n k)).

Definition nds_FA n k:=
 \osup (Zo Bnat (fun z => exists X, [/\ nds_ax X n, nds_card n X = z
     & nds_type X n k])).

Lemma nds_type_p1 X n k1 k2: inc n Bnat ->
  (nds_type X n k1) -> (nds_type X n k2) -> k1 = k2.
Proof.
rewrite /nds_type /nds_type'; move=> nB p1 p2.
case: p1; move => [pa pb]; case: p2; move => [pc pd].
+ by rewrite pa pc.
+ by move: pb pd=> [i id vz] [pd _]; move: (proj2 (pd _ id)); case.
+ by move: pb pd => [pb _] [i id iz]; move: (proj2 (pb _ id)); case.
+ move: pb pd => [qa [m [om qb qc]]] [_ [p [op qd qe]]].
  suff mp: m = p by rewrite -qc -qe mp.
  move: qc; set T1 := Zo _ _ => qc.
  have : \1c <=c (cardinal T1) by apply: card_ge1; fprops; ue.
  move /card_le1P => [i] /Zo_P [/(BintP nB) /qd le1 mv].
  move: qe; set T2 := Zo _ _ => qe.
  have : \1c <=c (cardinal T2) by apply: card_ge1; fprops; ue.
  move /card_le1P => [j] /Zo_P [/(BintP nB) /qb le2 pv].
  rewrite pv in le2; rewrite mv in le1; ord_tac.
Qed.

Lemma nds_type_p2 X n: inc n Bnat -> n <> \0c -> nds_ax X n ->
  exists2 k, k <=c n & nds_type X n k.
Proof.
move => nB nnz ax.
case: (p_or_not_p (nds_type0 X n)) => h.
  exists \0c; fprops;left; split => //.
set E:= fun_image (Bint n) (fun i => the_CNF_degree (X i)).
set m := intersection E.
set F := (Zo (Bint n) (fun i => the_CNF_degree (X i) = m)).
have s1: sub F (Bint n) by apply Zo_S.
move: (sub_smaller s1); rewrite (card_Bint nB) => le1.
have osE: ordinal_set E.
  rewrite /E; move=> t /funI_P [z /(BintP nB) /ax zi ->].
  by apply: OS_the_CNF_degree.
have neE: nonempty E.
  apply:funI_setne; exists \0c.
  apply /(BintP nB);split; [ apply: czero_least | ]; fprops.
move: (ordinal_setI neE osE); rewrite -/m => mE.
have om: ordinalp m by apply:osE.
have neF: nonempty F.
  by move: mE => /funI_P [z zn zv]; exists z; apply: Zo_i.
set k := cardinal F.
exists k => //; right; split => //.
  by apply: (cardinal_nonemptyset1 neF).
split.
  move => i lin; case: (ord_zero_dichot (ax _ lin)) => //.
  by move => baa;case: h; exists i.
exists m; split => // i /(BintP nB) lin.
have uE: inc (the_CNF_degree (X i)) E by apply /funI_P; ex_tac.
by split; [ exact | apply: osE | apply:setI_s1].
Qed.

Lemma nds_FA_ex n k:
   inc n Bnat -> n <> \0c -> k <=c n -> nds_FA n k <> \0c.
Proof.
move => nB nz klen.
rewrite /nds_FA.
have [X pa pb]: exists2 X, nds_ax X n & nds_type X n k.
  case (equal_or_not k \0c) => kz.
    rewrite kz; exists (fun z:Set => \0o).
      move => i _ /=; fprops.
    left; split => //; exists \0c => //; apply: card_ne0_pos; fprops.
  pose X i := Yo (i <c k) \1o omega0.
  have ha: nds_ax X n by move => t _; rewrite /X; Ytac h; fprops.
  have hb:forall i, i <c n -> \0o <o X i.
    move => i _; rewrite /X; Ytac h; [apply: ord_lt_01| apply: ord_lt_0omega].
  exists X => //; right; split => //; split => //.
  move: the_CNF_degree_one the_CNF_degree_omega => dg1 dgo.
  exists \0o; split; fprops.
  + move => i /ha/OS_the_CNF_degree h; ord_tac1.
  + set E := Zo _ _.
    move:(BS_le_int klen nB) => kB.
    have ->: E = (Bint k).
      set_extens t.
        move => /Zo_P [ /(BintP nB) lth]; rewrite /X; Ytac h1.
          by move => _; apply/(BintP kB).
        by rewrite dgo => ba; case: card1_nz.
      move => /(BintP kB) ltl;apply: Zo_i.
        apply /(BintP nB); co_tac.
      by rewrite /X; Ytac0; rewrite dg1.
   by rewrite (card_Bint kB).
set E := Zo Bnat _.
have ce: cardinal_set E by move => i /Zo_S /CS_Bnat.
move: (nds_c X nB) => [pc pd].
have zE: inc (nds_card n X) E.
   apply/Zo_i => //; exists X => //.
by move: (card_sup_ub ce zE) => /(card_leT pc) /card_ge1P[_ /nesym].
Qed.

Lemma nds_type_p3 n k (v := nds_FA n k):
  inc n Bnat -> n <> \0c -> k <=c n ->
  [/\ inc v Bnat,
   v <=c (nds_F n),
   (forall X, nds_ax X n -> nds_type X n k -> nds_card n X <=c v) &
   (exists X, [/\ nds_ax X n, nds_type X n k & nds_card n X = v])].
Proof.
move=> nB nz kn.
rewrite /v /nds_FA; set T:= Zo Bnat _.
have ta: sub T Bnat by apply: Zo_S.
have tb: inc (nds_F n) Bnat by move: (nds_j nB) => [ok _].
have tc: (forall i, inc i T -> i <=c (nds_F n)).
  move => i /Zo_P [_ [X [ax <- _]]].
  by move: (nds_j nB) => [_ _ _ p4]; apply: p4.
move: (Bnat_sup_pr ta tb tc) => [pa pb pc pd].
have pe: forall X, nds_ax X n -> inc (nds_card n X) Bnat.
  move: (BS_factorial nB) => tb1.
  move=> X ax; move: (nds_a X nB) => le1; apply: (BS_le_int le1 tb1).
split => //.
  by move=> X ax ax2; apply: pc; apply: Zo_i; [by apply: pe | exists X ].
case: pd; last by move /Zo_P=> [_ [X [p1 p2 p3]]];exists X; split.
move => te.
by move: (nds_FA_ex nB nz kn); rewrite /nds_FA -/T te setU_0; case.
Qed.

Lemma nds_type_p4 n (g := nds_FA n) (f:= nds_F n):
 inc n Bnat -> n <> \0c ->
 [/\ (forall k, k <=c n -> (g k) <=c f),
     (exists2 k, k <=c n & (g k) = f) &
     f= \osup (fun_image (Bintc n) g) ].
Proof.
move=> nB nz.
have pa: (forall k : Set, k <=c n -> g k <=c f).
  by move => k kn; move: (nds_type_p3 nB nz kn) => [_ pa _].
move: (nds_j nB); rewrite -/f; move=> [_ _ [X x1 x2] pd].
move: (nds_type_p2 nB nz x1) => [k kn kt].
move: (nds_type_p3 nB nz kn) => [_ _ pe pf].
have pb: (exists2 k, k <=c n & g k = f).
  move: (pe _ x1 kt); rewrite x2 => qa.
  move: pf=> [Y [ax x3 x4]]; exists k => //.
   apply card_leA.
      rewrite /g - x4; apply: pd => //.
  by apply: (card_leT qa); apply card_leR; move: qa => [_ ok _].
split => //.
have oT: ordinal_set (fun_image (Bintc n) g).
  move=> t /funI_P [z zc ->].
  by move: zc => /(BintcP nB) => kn1; move: (pa _ kn1) => [[ok _] _].
apply: ord_leA.
  move: pb=> [s sn sv].
  apply: ord_sup_ub => //; apply /funI_P; exists s => //.
  by apply /(BintcP nB).
apply: ord_ub_sup => //.
   by move: (pa _ kn) => [_ [ok _] _].
move=> t /funI_P [z zc ->]; move: zc => /(BintcP nB) => zc.
exact: (ordinal_cardinal_le (pa _ zc)).
Qed.

Lemma nds_type_p5 n X:
  inc n Bnat -> nds_ax X n -> nds_type0 X n ->
  exists Y,
    [/\ nds_ax Y n, nds_card n X = nds_card n Y & Y (cpred n) = \0o].
Proof.
move => nB ax [i lin vz].
set E := (Bint n).
move /(BintP nB):(lin) => ii.
move: (card_le_ltT (czero_least (proj31_1 lin)) lin) => np.
case: (equal_or_not i (cpred n)) => ip.
  exists X; split; [exact | exact |ue].
pose g j := Yo (j = i) (cpred n) (Yo (j = (cpred n)) i j).
have pa: g (cpred n) = i by rewrite /g; Ytac0; Ytac0.
have nz:= (nesym (proj2 np)).
move: (cpred_pr nB nz) => [pb pc].
have axx: cpred n <c n by rewrite {2} pc; apply: card_lt_succ.
have ta: lf_axiom g E E.
  move=> t /(BintP nB) => h; apply /(BintP nB).
  by rewrite /g; Ytac h1 => //; Ytac h2.
set G:= Lf g E E.
have qc: inc (cpred n) E by apply /(BintP nB).
have bg: bijection G.
  apply: lf_bijective => //.
   move=> u v ue ve; rewrite /g; Ytac h1; Ytac h2.
   + by rewrite h1 h2.
   + Ytac h3; [ by rewrite h3 h1 | by move=> eq; case: h3 ].
   + by rewrite h2; Ytac h3; [ move => <-| Ytac h4; [| move=> h; case: h3]].
   + by Ytac h3; [ move=> h4; case: h2 | Ytac h4;[ move => h5; case: h1 |]].
  move=> y yE; rewrite /g.
  case: (equal_or_not y (cpred n)) => qa.
    by exists i=> //; Ytac0; Ytac0.
  case: (equal_or_not y i) => qb.
    exists (cpred n) => //;Ytac0; Ytac0 => //.
  by exists y => //; Ytac0; Ytac0.
have qx: function (Lf g E E) by apply: lf_function.
have GE: inc G (permutations E).
   apply: Zo_i => //; apply /fun_set_P;split => //; rewrite /G; aw.
have ax2:= proj1(nds_b nB ax GE).
exists (fun z => X (Vf G z)).
by rewrite - (nds_m nB ax GE) {2}/G /g; aw; Ytac0; Ytac0; split.
Qed.

Lemma nds_type_p6 n X: inc n Bnat -> nds_ax X (succ n) -> X n = \0o ->
  nds_card (succ n) X = nds_card n X.
Proof.
move => nB ax nz.
have snB := BS_succ nB.
set I := Bint n.
set I' := Bint (succ n).
have IP: forall i, inc i I <-> i <c n by move => i; exact: (BintP nB).
have IP': forall i, inc i I' <-> i <c (succ n)
      by move => i; exact: (BintP snB).
have H0:=(card_lt_succ_leP nB).
have nn:= card_lt_succ nB.
have nI': inc n I' by apply /IP'.
have Ha: forall i, i <=c n -> i <> n -> inc i I.
  move => i lein nin; apply /IP; split => //.
rewrite /nds_card; apply:f_equal; set_extens z; last first.
  move => /funI_P [f /Zo_P [ /fun_set_P [ff sf tf] bf] ->].
  have Hb: forall i, i <=c n -> i <> n -> Vf f i <c n.
    move => i lein nin; move: (Ha _ lein nin); rewrite /I- sf => isf.
    by move:(Vf_target ff isf); rewrite tf => /IP.
  pose g z := Yo (z = n) n (Vf f z).
  have ta: lf_axiom g I' I'.
    move => i /IP' /H0 isn;apply /IP'; rewrite /g; Ytac h; fprops.
    exact: (card_lt_ltT (Hb _ isn h) nn).
  have bg: bijection (Lf g I' I').
    apply: lf_bijective => //.
      move => u v /IP' /H0 lun /IP' /H0 lvn.
      rewrite /g; Ytac h1; Ytac h2.
      + by rewrite h1 h2.
      + by move: (nesym (proj2 (Hb _ lvn h2))).
      + by move: (proj2 (Hb _ lun h1)).
      + by apply: (proj2 (proj1 bf)); rewrite sf; apply: Ha.
    move => y yI; case (equal_or_not y n) => eyn.
      by exists y => //; rewrite eyn /g; Ytac0.
    move:yI => /IP' /H0 lyn.
    move: (Ha _ lyn eyn); rewrite /I - tf => /(proj2 (proj2 bf)).
    rewrite sf - /I; move => [x /IP xsf <-].
    move: (card_lt_ltT xsf nn) => /IP'; rewrite -/I' => xi'.
    by move: (proj2 xsf) => lxn; ex_tac;rewrite /g; Ytac0.
  apply/funI_P; exists (Lf g I' I').
     apply/Zo_i => //;apply/fun_set_P; split; [ fct_tac | aw | aw].
  rewrite /nds_sc (osum_expansion_succ _ nB) {1} /g; aw; Ytac0; rewrite nz.
  set A := osum_expansion _ _; set B := osum_expansion _ _.
  have <-: A = B.
     apply: (osum_expansion_exten nB) => i lin; rewrite /g.
     have ii: inc i I' by apply /IP'; co_tac.
     by aw; move: (proj2 lin) => nin; Ytac0.
  have oA: ordinalp A.
     apply: (OS_osum_expansion nB) => i lin; apply: ax.
     move: (Hb _ (proj1 lin) (proj2 lin)) => h2; co_tac.
  by rewrite (osum0l oA).
move => /funI_P [f /Zo_P [ /fun_set_P [ff sf tf] bf] ->].
have ntf: inc n (target f) by rewrite tf; apply /(BintP snB).
set i0:= Vf (inverse_fun f) n.
have fif: function (inverse_fun f) by apply: bijective_inv_f.
have i0sf: inc i0 (source f) by rewrite -ifun_t /i0; Wtac; rewrite ifun_s.
have fi0: Vf f i0 = n by rewrite /i0; rewrite (inverse_V bf ntf).
move: (proj2 (proj1 bf)) => iif.
case (equal_or_not i0 n) => ei0n.
  set f0:= Lf (Vf f) I I.
  have axf: lf_axiom (Vf f) I I.
    move => i /IP lin; apply/IP.
    have isf: inc i (source f) by rewrite sf; apply/IP'; co_tac.
    move: (Vf_target ff isf); rewrite tf => /IP' /H0 le1.
    case (equal_or_not (Vf f i) n) => eq1; last by split.
    rewrite - eq1 in fi0.
    move: (iif _ _ i0sf isf fi0) => h1.
    by case (proj2 lin); rewrite - h1 ei0n.
  have fp: inc f0 (permutations (Bint n)).
    apply: Zo_i.
      by rewrite /f0;apply/fun_set_P; split; aw;apply:lf_function.
    apply:lf_bijective => //.
      move => u v /IP ui /IP vp; apply:(iif u v);rewrite sf; apply /IP';co_tac.
    move => y /IP yp.
    have ytf: inc y (target f) by rewrite tf; apply /IP'; co_tac.
    move:(proj2 (proj2 bf) _ ytf) => [x xsf eq1]; exists x => //.
    move: xsf;rewrite sf => /IP' /H0 xn.
    by apply /IP; split => //exn; move:(proj2 yp); rewrite -eq1 - fi0 exn ei0n.
  apply/funI_P; exists f0; first exact.
  rewrite /nds_sc (osum_expansion_succ _ nB) - {1} ei0n fi0 nz.
  set A := osum_expansion _ _.
  have oA: ordinalp A.
     apply: (OS_osum_expansion nB) => i lin; apply: ax.
     apply/IP'; rewrite /I' - tf; Wtac; rewrite sf;apply/IP'; co_tac.
   rewrite (osum0l oA); apply: (osum_expansion_exten nB).
   move => i /IP lin /=; rewrite /f0; aw.
have li0n: i0 <=c n.
  apply /H0; apply/IP'; rewrite /i0 /I'- sf - ifun_t.
  by apply:Vf_target => //;rewrite ifun_s.
move/(card_le_succ_succP (proj31 li0n) (proj32 li0n)): (li0n) => li0n1.
move: (cdiff_pr li0n1)(BS_diff (succ i0) snB).
set m := (succ n -c succ i0) => sa mB.
have iB:=(BS_le_int li0n nB).
have siB:=(BS_le_int li0n1 snB).
have sb : i0 +c m = n.
  apply: (succ_injective1 (CS_sum2 i0 m) (CS_Bnat nB)).
  by rewrite - (csum_via_succ1 _ iB) sa.
pose g i := Yo (i <c i0) (Vf f i) (Vf f (succ i)).
pose g0 i := X (Vf (Lf g I I) i).
pose f0 i := X (Vf f i).
have axg: lf_axiom g I I.
  move => i /IP lin; rewrite /g; Ytac h; apply /IP => //.
    have isf: inc i (source f) by rewrite sf; apply /IP'; co_tac.
    move: (Vf_target ff isf); rewrite tf => /IP' /H0 ha; split; first exact.
    rewrite - fi0 => h1; move: (iif _ _ isf i0sf h1) => h2.
    by case: (proj2 h).
  have isf: inc (succ i) (source f).
    by rewrite sf; apply /IP'; apply /(card_succ_succ_ltP(BS_lt_int lin nB) nB).
  move: (Vf_target ff isf); rewrite tf => /IP' /H0 ha; split; first exact.
  rewrite - fi0 => h1; move: (iif _ _ isf i0sf h1) => h2.
  by case: h; rewrite - h2; apply:(card_lt_succ (BS_lt_int lin nB)).
have ax1: ord_below_n f0 (succ i0 +c m).
  rewrite sa => i lin; rewrite /f0; apply: ax; apply/(BintP snB).
  by Wtac; rewrite sf; apply/(BintP snB).
have ax2: (ord_below_n g0 (i0 +c m)).
   rewrite sb => i /IP lin; rewrite /g0; aw; apply ax.
   move: (axg _ lin) => /IP h1 ; co_tac.
have osa: ordinalp (osum_expansion f0 i0).
  apply: (OS_osum_expansion iB) => i lin; rewrite /f0; apply: ax.
  apply/(BintP snB); Wtac; rewrite sf;apply/(BintP snB).
  exact: (card_lt_ltT lin (card_le_ltT li0n nn)).
have -> : nds_sc (succ n) X f = nds_sc n X (Lf g I I).
  move: (osum_expansionA siB mB ax1); rewrite sa -/(nds_sc _ _ _) => ->.
  rewrite (osum_expansion_succ _ iB) {2} /f0 fi0 nz (osum0l osa).
  rewrite /nds_sc - sb (osum_expansionA iB mB ax2); apply: f_equal2.
     apply:(osum_expansion_exten mB) => i lim; rewrite /f0/g0 /g.
     have ha: inc (i +c i0) I.
       apply /IP; rewrite - sb (csumC _ m); apply:(csum_Mlteq iB mB lim).
     have hb: ~(i +c i0 <c i0).
       move:(csum_M0le i (proj31 li0n)); rewrite csumC => ua ub; co_tac.
     by aw; Ytac0; rewrite (csum_via_succ _ iB).
   apply:(osum_expansion_exten iB) => i lim; rewrite /f0/g0 /g.
   aw; [ by Ytac0 |apply /IP; co_tac].
apply /funI_P; exists (Lf g I I) => //; apply: Zo_i.
  by apply/fun_set_P; split; aw; apply:lf_function.
apply: lf_bijective => //.
  move => u v /IP ui /IP vi.
  have usf: inc u (source f) by rewrite sf;apply/IP'; co_tac.
  have vsf: inc v (source f) by rewrite sf;apply/IP'; co_tac.
  move:(BS_lt_int ui nB) (BS_lt_int vi nB) => uB vB.
  have u'sf: inc (succ u) (source f).
    by rewrite sf;apply/IP';apply/(card_succ_succ_ltP uB nB).
  have v'sf: inc (succ v) (source f).
    by rewrite sf;apply/IP';apply/(card_succ_succ_ltP vB nB).
  rewrite /g; Ytac h1; Ytac h2 => eq.
  + by apply: (proj2 (proj1 bf) _ _ usf vsf).
  + move: (proj2 (proj1 bf) _ _ usf v'sf eq) => e2.
    move: h1; rewrite e2 => e3; case h2; move: (card_le_succ vB) => e4; co_tac.
  + move: (proj2 (proj1 bf) _ _ u'sf vsf eq) => e2.
    move: h2;rewrite - e2 => e3; case h1; move: (card_le_succ uB) => e4; co_tac.
  + move: (proj2 (proj1 bf) _ _ u'sf v'sf eq).
    by move => /(succ_injective1 (proj31_1 ui) (proj31_1 vi)).
move => y /IP yi.
have ytf: inc y (target f) by rewrite tf; apply/IP'; co_tac.
move: (proj2 (proj2 bf) _ ytf) => [x xsf ea]; rewrite - ea.
move: xsf; rewrite sf => /IP' xsn.
have xB:= (BS_lt_int xsn snB).
case: (Bnat_to_ell iB xB) => cix.
+ by move:(f_equal (Vf f) cix); rewrite fi0 ea; move => eb; case: (proj2 yi).
+ case (equal_or_not x \0c) => xnz.
    rewrite xnz in cix;case:(card_lt0 cix).
  move: (cpred_pr xB xnz) => [sc sd].
  move: xsn; rewrite sd; move/(card_succ_succ_ltP sc nB) => /IP ci.
  exists (cpred x) => //; rewrite - sd /g; Ytac h; last by rewrite - sd.
 move/(card_le_succ_lt0P (CS_Bnat sc) iB):h; rewrite - sd => ha; co_tac.
exists x; [ apply /IP; co_tac | by rewrite /g; Ytac0].
Qed.

Lemma nds_type_p7 n: inc n Bnat -> nds_FA (succ n) \0c = nds_F n.
Proof.
move => nB.
move: (nds_type_p3 (BS_succ nB) (@succ_nz n) (czero_least (CS_succ n))).
move => [pa pb pc pd].
move:pd => [X0 [aX0 Xt0 Xv]].
move: Xt0; case; [move => [_ pe] | by case].
move: (nds_type_p5 (BS_succ nB) aX0 pe) => [X2 [ax2 X2v X20]].
have pg': X2 n = \0o by move:X20; rewrite (cpred_pr2 nB).
move: Xv; rewrite X2v => eq0.
clear pe aX0 X20 X2v.
have r1:= (nds_type_p6 nB ax2 pg').
move: (nds_j nB) => [sa sb [X4 ax4 eq1] sd].
set X5 := fun z => Yo (z = n) \0o (X4 z).
have ax5: nds_ax X5 (succ n).
  move => i /(card_lt_succ_leP nB) lin; rewrite /X5; Ytac h; fprops; apply: ax4.
  split => //.
have X5n: X5 n = \0c by rewrite /X5; Ytac0.
have ax3: nds_ax X2 n.
   move => i lin; apply: (ax2 i (card_lt_ltT lin (card_lt_succ nB))).
have nd5: nds_type X5 (succ n) \0c.
  by rewrite /X5;left; split => //; exists n; fprops; Ytac0.
have r2:= (nds_type_p6 nB ax5 X5n).
have r3: nds_card n X5 = nds_card n X4.
  rewrite /nds_card/nds_sums; apply: f_equal.
   have H: forall z i, inc z (permutations (Bint n)) -> i <c n
     -> (Vf z i <> n).
     move => z i /Zo_P [] /fun_set_P [fz sz tz] bz /(BintP nB).
     rewrite - sz => isz; move: (Vf_target fz isz); rewrite tz.
     by move/(BintP nB) => [_].
  by set_extens t; move /funI_P => [z zp ->]; apply/funI_P; ex_tac;
    apply:(osum_expansion_exten nB) => i lin; move: (H _ _ zp lin) => w;
    rewrite /X5; Ytac0.
apply: card_leA; first by move: (sd _ ax3); rewrite - eq0 r1.
by move: (pc _ ax5 nd5); rewrite r2 r3 eq1.
Qed.

Lemma nds_type_p8 n: inc n Bnat -> nds_FA (succ n) (succ n) = (succ n).
Proof.
move => nB.
move: (nds_type_p3 (BS_succ nB) (@succ_nz n) (card_leR (CS_succ n))).
set v := (nds_FA (succ n)).
move => [vB vle va vb].
move: (nds_q3 nB) => [X[pa pb pc pd]].
have pe: nds_type X (succ n) (succ n).
  right; split; first by apply: succ_nz.
  split => //; exists \1o; split.
   + apply: OS1.
   + move => i/(card_lt_succ_leP nB) /pc ->; fprops.
   + set E := Zo _ _.
     have ->: E = Bint (succ n).
       apply: extensionality;[ apply: Zo_S | move => t ti; apply: Zo_i => //].
       by apply:pc; apply /(BintsP nB).
     by rewrite (card_Bint (BS_succ nB)).
move: (va _ pa pe); rewrite pd => le1.
move: vb => [Y [ay ty yv]].
case ty; [ by move :(@succ_nz n) => sp [h _] | move => [_ [ty1 ty2]]].
move:ty2 => [m [om mp1 mp2]].
have pg:forall i, i<=c n -> the_CNF_degree (Y i) = m.
  move: mp2; set I := (Bint (succ n)).
  have ci: cardinal I = succ n by rewrite (card_Bint (BS_succ nB)).
  have fsI: finite_set I. rewrite /finite_set ci; apply:(Bnat_hi (BS_succ nB)).
  set E := Zo _ _ => ce.
  have seI: sub E I by apply: Zo_S.
  move: (cardinal_setC4 seI fsI);rewrite ci ce cdiff_n_n.
  move /cardinal_nonemptyset => H.
  move => i /(BintsP nB) iI; ex_middle bad.
  by empty_tac1 i; apply /setC_P; split => // /Zo_hi.
have pf: forall i, i<=c n -> \0o <o (Y i).
  by move => i /(card_lt_succ_leP nB) /ty1.
by move: (nds_q2 nB pf pg); rewrite yv => le2; apply: card_leA.
Qed.

Lemma nds_type_p9_aux a b i j:
  ordinalp a -> ordinalp b -> i <o omega0 -> j <o omega0 ->
  exists2 k, k <o omega0 &
      (omega0 *o a +o i) +o (omega0 *o b +o j) = (omega0 *o (a +o b) +o k).
Proof.
move: OS_omega => oo oa ob ip jp.
move: (proj31_1 ip)(proj31_1 jp) => oi oj.
have oA :=OS_sum2 (OS_prod2 oo oa) oi.
have ooa:= OS_prod2 oo oa.
have oob:= OS_prod2 oo ob.
rewrite (osumA oA oob oj) - (osumA ooa oi oob).
case: (ord_zero_dichot ob) => bp.
   exists (i +o j); first by apply:osum2_lt_omega.
   by rewrite bp oprod0r (osum0r oa) (osum0r oi) osumA.
exists j => //.
move: (odiff_pr (oprod_Mle1 oo bp)) => [pb pc]; rewrite pc.
by rewrite (osumA oi oo pb) (osum_int_omega ip) - pc (osum_prodD oa ob oo).
Qed.

Lemma nds_type_p9 n (X:fterm) (Y:= fun i => succ_o (omega0 *o (X i))):
  inc n Bnat -> nds_ax X n -> nds_card n X <=c nds_card n Y.
Proof.
move => nB aX.
have pa: forall z, inc z (perm_int n) ->
    exists k, (ord_div_pr0 (nds_sc n Y z) omega0 (nds_sc n X z) k).
  move => s /perm_intP [[[fs _] _] sf tf]; rewrite /Y /nds_sc.
  have: forall z, z<c n -> ordinalp (X (Vf s z)).
     move => z /(BintP nB) zb; apply: aX; apply/(BintP nB); Wtac.
  move: (n) nB; apply: cardinal_c_induction.
     have o0 := OS0.
     move => _; exists \0o;hnf;rewrite !osum_expansion0 oprod0r (osum0r OS0).
     split => //; by exact ord_lt_0omega.
  move => m mB Hrec h1.
  have mm:= card_lt_succ mB.
  have /Hrec [k [oa kb kv kp]]: (forall z, z <c m -> ordinalp (X (Vf s z))).
    move => z zm; apply:h1 => //; co_tac.
  rewrite ! (osum_expansion_succ _ mB) kv.
  set a := osum_expansion _ _.
  have ob := h1 _ mm.
  rewrite - (ord_succ_pr (OS_prod2 OS_omega ob)).
  move:(nds_type_p9_aux ob oa ord_lt_1omega kp) => [k2 k2p ->].
  exists k2; split; [ by apply: OS_sum2 | ord_tac | exact | exact ].
have pb: forall z, inc z (perm_int n) ->
     nds_sc n X z = P (oquorem (nds_sc n Y z) omega0).
  move => z zp; move:(pa _ zp) => [k kp].
  have o1:ordinalp(nds_sc n Y z) by move: (kp) => [ra rb -> _]; fprops.
  exact (proj1 (oquoremP2 o1 ord_lt_0omega kp)).
rewrite /nds_card /nds_sums.
set F := fun_image _ _; set E := fun_image _ _.
pose f x := P (oquorem x omega0).
have ax: forall x, inc x E -> inc (f x) F.
  by move => x /funI_P [z zp ->]; apply/funI_P; ex_tac; rewrite /f - pb.
have sjf: surjection(Lf f E F).
  apply: lf_surjective => //.
  move => y /funI_P [z zp ->]; rewrite (pb _ zp).
  exists (nds_sc n Y z) => //; apply/funI_P; ex_tac.
move: (image_smaller_cardinal (proj1 sjf)).
rewrite surjective_pr0; aw.
Qed.

Lemma nds_type_p10 n: inc n Bnat ->
  exists X, [/\ nds_ax X n, forall i, i <c n -> \0o <o X i &
      nds_card n X = nds_F n].
Proof.
move => nB; move:(nds_j nB) => [ _ _ [X ax xv] pb].
move: (nds_type_p9 nB ax).
set Y := (fun i => succ_o (omega0 *o X i)) => r1.
have ha: forall i, i <c n -> \0o <o Y i.
  move => i /ax ox; apply:ord_lt0_succ;apply: (OS_prod2 OS_omega ox).
have hb: nds_ax Y n by move => t /ha h;ord_tac.
move: (pb _ hb) => hc; rewrite xv in r1.
by exists Y; split => //; apply: card_leA.
Qed.

Lemma nds_type_p11 n (g := nds_FA n) (f:= nds_F n):
 inc n Bnat -> n <> \0c ->
   (forall k, k <=c n -> k <> \0c -> (g k) <=c f) /\
   (exists k, [/\ k <=c n, k <> \0c & (g k) = f]).
Proof.
move => pa pb; move:(nds_type_p4 pa pb) => [pc _ _].
split; first by move => k kn _; apply: pc.
move: (nds_type_p10 pa) => [X [ax1 ax2 xv]].
move: (nds_type_p2 pa pb ax1) => [k1 k1n tX].
move:(nds_type_p3 pa pb k1n) => [_ _ qa _].
move: (qa _ ax1 tX); rewrite xv => le1.
case: tX; first by move => [_ [i lin xi]]; case: (proj2 (ax2 _ lin)).
move => [knz _]; exists k1; split => //.
exact: (card_leA (pc _ k1n) le1).
Qed.

Definition nds_tn_S X n:=
   unionf (powerset (Bint n)) (fun K =>
      fun_image (perm_int (cardinal K))
         (fun s => nds_sc (cardinal K) (fun z => X (nth_elt K z)) s)).
Definition nds_tn_C X n := cardinal (nds_tn_S X n).
Definition ndstnC n := succ (n *c (\2c ^c (cpred n))).

Definition nds_tn_ax X n :=
    (forall i, i<c n -> \0o <o X i) /\
    exists2 e, ordinalp e & forall i, i<c n -> the_CNF_degree (X i) = e.

Definition nds_tn_sup n :=
  \osup(Zo Bnat (fun z => exists2 X, nds_tn_ax X n & nds_tn_C X n = z)).

Lemma nds_tn1 X n:
   inc n Bnat -> nds_ax X n ->
   nds_tn_C X n <=c (\2c ^c n) *c (factorial n).
Proof.
move => nB ax.
rewrite /nds_tn_C /nds_tn_S. set F:= (fun K : Set => _).
set pIn := (powerset (Bint n)).
set g1:= (Lg pIn (fun a : Set => cardinal (Vg (Lg pIn F) a))).
move: (csum_pr1_bis pIn F).
have <-: card_sum g1 = card_sumb pIn (fun a : Set => cardinal (F a)).
  rewrite /card_sumb;apply:f_equal;apply:Lg_exten => t tx; bw.
set g2 := cst_graph pIn (factorial n).
have sd: domain g1 = domain g2 by rewrite /g1/g2; bw.
have le1:forall x, inc x (domain g1) -> Vg g1 x <=c Vg g2 x.
   rewrite /g1 /g2; bw => K KB; bw; move/setP_P:KB => KB.
  move:(sub_smaller KB); rewrite (card_Bint nB) => ka.
  have nKB:=(BS_le_int ka nB).
  move: (factorial_monotone nB ka); apply: card_leT.
  move:(number_of_permutations (finite_Bint (cardinal K))).
  rewrite -/(perm_int _) (card_Bint nKB) => <-.
  apply:fun_image_smaller.
move:(csum_increasing sd le1).
rewrite csum_of_same cprodC - cprod2_pr2a card_setP - cpow_prb (card_Bint nB).
move => ha hb; exact:(card_leT hb ha).
Qed.

Lemma nds_tn2 n (f:= nds_tn_sup n): inc n Bnat ->
  [/\ inc f Bnat, \0c <c f, f <=c (\2c ^c n) *c (factorial n),
  (exists2 X, nds_tn_ax X n & nds_tn_C X n = f) &
  (forall X, nds_tn_ax X n -> nds_tn_C X n <=c f)].
Proof.
move => nB.
rewrite /f /nds_tn_sup; set T := Zo _ _.
have TB: sub T Bnat by apply: Zo_S.
have kB:=(BS_prod (BS_pow BS2 nB) (BS_factorial nB)).
set k := \2c ^c n *c factorial n.
have H: forall X, nds_tn_ax X n -> nds_tn_C X n <=c k.
  by move => X [ax _]; apply:(nds_tn1 nB) => i /ax /proj32_1.
have H1:forall X, nds_tn_ax X n -> inc (nds_tn_C X n) Bnat.
  move => X x1; exact:(BS_le_int (H _ x1) kB).
have ks:forall i, inc i T -> i <=c k by move => z /Zo_hi [X /H ax <-].
pose X (i:Set):= omega0.
have ax: nds_tn_ax X n.
  split; first by move => i _; apply: ord_lt_0omega.
  exists \1o; [ apply: OS1 | move => i _; apply:the_CNF_degree_omega].
have ta: inc (nds_tn_C X n) T by apply: (Zo_i (H1 _ ax)); exists X.
have ha: \0c <c union T.
  have: nonempty (nds_tn_S X n).
    set K:= Bint n; have idp:=(perm_int_id n).
    exists (nds_sc (cardinal K) (fun z => X (nth_elt K z)) (identity (Bint n))).
    apply/setUf_P; exists K; first by apply:setP_Ti.
    rewrite /K (card_Bint nB);apply/funI_P;ex_tac.
  move /cardinal_nonemptyset1; rewrite -/(nds_tn_C X n) => h0.
  have cst:cardinal_set T by move => t /TB /CS_Bnat.
  exact:(card_lt_leT (card_ne0_pos (cst _ ta) h0) (card_sup_ub cst ta)).
move: (Bnat_sup_pr TB kB ks) => [pa pb pc pd];split => //; last first.
  move => Y x1; apply: pc; apply/ Zo_P; split; [by apply: H1 | by exists Y].
by case:pd => h1; [ empty_tac1 (nds_tn_C X n) | exact: (Zo_hi h1)].
Qed.

Lemma nds_tn3: nds_tn_sup \0c = \1c.
Proof.
move:(nds_tn2 BS0); rewrite factorial0 cpowx0 (cprod1r CS1).
set f := nds_tn_sup \0c.
move =>[pa /card_ge1P pb px _ _]; co_tac.
Qed.

Lemma nth_set11 K a (f:= nth_elt K)(g:= nth_elt (K +s1 a)) (q:= cardinal K) :
  sub K Bnat -> finite_set K -> inc a Bnat ->
  (forall i, inc i K -> i <c a) ->
  (forall i, i<c q -> f i = g i) /\ g q = a.
Proof.
move => KB fsK aB Ha.
have anK: ~ inc a K by move => /Ha [].
move:(card_succ_pr anK); set q1:= cardinal (K +s1 a);rewrite -/q => qv.
have K1B: sub (K +s1 a) Bnat by move => t /setU1_P; case; [apply: KB | move ->].
have qB: inc q Bnat by apply /BnatP.
have q1B: inc q1 Bnat by rewrite qv; fprops.
move:(nth_set6 qB KB) (nth_set6 q1B K1B); rewrite -/q -/q1 qv => sa sb.
suff aux: forall i, i<=c q -> nth_elts K i = nth_elts (K +s1 a) i.
  rewrite /f/g /nth_elt.
  split.
    move => i liq.
    move/(card_le_succ_ltP _ (BS_lt_int liq qB)): (liq) => /aux ->.
    by rewrite (aux _ (proj1 liq)).
  have hb: ((K +s1 a) -s K) = singleton a.
    apply:set1_pr; first by apply/setC_P; split; fprops.
    by move => z /setC_P [/setU1_P ha hb]; case: ha.
  by rewrite - (aux _ (card_leR (CS_Bnat qB))) sb sa hb setU_1.
move => i ilq; move:(BS_le_int ilq qB) => iB.
move: i iB ilq; apply: cardinal_c_induction.
   by rewrite /nth_elts !induction_term0.
move => n nB Hrec sc.
rewrite (nth_elts_succ _ nB) (nth_elts_succ _ nB).
have lenk:=(card_leT (card_le_succ nB) sc).
rewrite - (Hrec lenk).
move:(nth_set5 nB KB lenk) => [[]].
rewrite /nth_more; set S1 := (nth_elts K n) => ha hb hc.
have s1: sub (K -s S1) Bnat by move => t /setC_P [/KB].
have s2: sub ((K +s1 a) -s S1) Bnat by move => t /setC_P [/K1B].
case:(emptyset_dichot (K -s S1)) => ne1.
  move:(cardinal_setC4 ha fsK); rewrite - /q hc ne1 cardinal_set0.
  by move: (nesym (cdiff_nz (card_lt_leT (card_lt_succ nB) sc))).
have ne2: nonempty ((K +s1 a) -s S1).
   by exists a; apply/setC_P; split; [ fprops | move/ha].
move:(nth_set1 s1 ne1); set y1:= intersection _; move => [/setC_P[hu hv] pb].
move:(nth_set1 s2 ne2); set y2:= intersection _; move => [pa' pb'].
apply: f_equal; apply:f_equal.
have /pb' y21: inc y1 ((K +s1 a) -s S1) by apply/setC_P; split; fprops.
move/setC_P:pa' => [/setU1_P hu1 hv1]; case: hu1=> hu1.
  move/(setC_P): (conj hu1 hv1) => /pb le1; co_tac.
move:(Ha _ hu); rewrite - hu1 => hu2; co_tac.
Qed.

Lemma nds_p2 n c K: inc n Bnat ->
   (forall i, i<c n -> inc (c i) Bnat) ->
   inc K (powerset (Bint n)) ->
   osum_expansion (fun z => c (nth_elt K z)) (cardinal K) =
    card_sumb K c.
Proof.
move => nB cIb /setP_P Kb.
have KB: sub K Bnat by apply: (sub_trans Kb (@Bint_S1 n)).
have fsK:=(sub_finite_set Kb (finite_Bint n)).
set q := cardinal K; set f := nth_elt K.
have qB: inc q Bnat by apply /BnatP.
have ha: forall i, i <c q -> inc (f i) K.
  move => i iq; apply:(nth_set9 (BS_lt_int iq qB) KB iq).
have: forall j, inc j K -> exists2 i, i <c q & j = f i.
  move => j jK; exact(nth_set_10 KB fsK jK).
have : forall i j, i <c q -> j <c q -> f i = f j -> i = j.
  move => i j /(BintP qB) iq /(BintP qB) jq.
  move:(proj2 (proj1 (proj1 (nth_set_fct_bf KB fsK)))).
  have ax: lf_axiom (nth_elt K) (Bint (cardinal K)) K.
    by move => t /(BintP qB) /ha.
  rewrite /nth_set_fct; aw => h; move: (h i j iq jq);aw.
have: forall i, inc i K -> inc (c i) Bnat by move => i /Kb /(BintP nB) /cIb.
move: q qB (f) (K) ha fsK; clear.
apply: cardinal_c_induction.
  move => k K _ _ _ _ sf.
  have h: domain (Lg K c) = emptyset.
    by bw; apply /set0_P => t /sf [i /card_lt0].
  by rewrite osum_expansion0 /card_sumb (csum_trivial h).
move => n nB Hrec f K fK fsK cB fi fs.
rewrite (osum_expansion_succ _ nB).
have nn:= (card_lt_succ nB).
move:(fK _ nn) => fnK.
move: (setC1_K fnK); set K1:= K -s1 (f n) => Kv.
have h1: forall i, i <c n -> inc (f i) K1.
  move => i lin; move:(card_lt_ltT lin nn) => h; move: (fK _ h).
  rewrite - Kv =>/setU1_P; case => // eq; move:(fi _ _ h nn eq) => ein.
  by case: (proj2 lin).
have h2:=(sub_finite_set (@sub_setC K (singleton (f n))) fsK).
have h3: forall i, inc i K1 -> inc (c i) Bnat by move => i /setC1_P [/cB].
have h4: forall i j, i <c n -> j <c n -> f i = f j -> i = j.
  move => i j lin ljn;apply (fi _ _ (card_lt_ltT lin nn) (card_lt_ltT ljn nn)).
have h5:forall j, inc j K1 -> exists2 i : Set, i <c n & j = f i.
  move => j /setC1_P [/fs [i /(card_lt_succ_leP nB) lin ->] h].
  case: (equal_or_not i n) => ein; first by case: h; rewrite ein.
  by exists i.
have fnk1:~ inc (f n) K1 by move/setC1_P=> [ _ ].
have skB: inc (card_sumb K1 c) Bnat.
  apply:finite_sum_finite; hnf; rewrite/allf;bw;split => //.
  by move => t tk1; bw; apply: h3.
rewrite (Hrec f K1 h1 h2 h3 h4 h5) - Kv (csumA_setU1 _ fnk1).
by rewrite (osum2_2int (cB _ fnK) skB) csumC.
Qed.

Lemma the_CNF_omega_kj j k (X := omega0 *o j +o k)
  (e := (the_CNF_degree X))
  (r:= CNFbvo (Vg (P (Q (the_CNF X))))
        (Vg (Q (Q (the_CNF X))))(cpred (P (the_CNF X))))
  (c:= (Vg (Q (Q (the_CNF X))) (cpred (P (the_CNF X))))):
  inc j Bnat -> inc k Bnat -> \0c <c j ->
  \0o <o X /\ [/\ e = \1o, c = j & r = k].
Proof.
move => /olt_omegaP kj /olt_omegaP ko /proj2 jp1.
have ok: ordinalp k by ord_tac.
have oj: ordinalp j by ord_tac.
have jp : \0c <o j by split; [ apply:ozero_least | exact].
have op:= (OS_prod2 OS_omega oj).
have ox: ordinalp X by apply: (OS_sum2 (OS_prod2 OS_omega oj) ok).
have xp: \0o <o X.
  apply: ord_ne0_pos => // sz.
  move: (osum2_zero op ok sz) => [p1 _].
  by case: (oprod2_nz OS_omega oj omega_nz (nesym jp1)).
split; first by exact.
case : (ord_zero_dichot ok) => kz.
   set ee := fun i: Set => \1o.
   set cc := fun i: Set => j.
   have ax: CNFb_axo ee cc \1c.
    split; first split.
    + apply: ord_le_2omega.
    + move => i lin; rewrite /ee; fprops.
    + by move => i lin; rewrite /cc.
    + by move => i iB /card_lt1 h; case: (@succ_nz i).
    + by move => i lin.
  move: (CNFbB_prop ax BS1); set y := (CNFbB \1c ee cc); move => [ax2 yv].
  have py2: P y = \1c by rewrite /y /CNFbB; aw.
  move: (CNFB_ax_simp ax2) => [_ ax4].
  move: BS0 card_lt_01 => b0 lt01.
  have eq1: X = CNFBv y.
    rewrite py2 in ax4.
    rewrite /X kz (osum0r op) /CNFBv py2 /CNFbvo.
    rewrite (CNFq_p3 (proj1 ax4) lt01) /cantor_mon.
    rewrite /y /CNFbB !(pr1_pair, pr2_pair) /e; bw; Ytac0.
    by rewrite (opowx1 OS_omega); Ytac0.
  move:(the_CNF_p0 ox) => [sa sb].
  rewrite - sb in eq1; rewrite py2 in ax4.
  rewrite /e/c /r /the_CNF_degree.
  rewrite (CNFB_unique sa ax2 eq1) py2 - succ_zero (cpred_pr1 CS0).
  rewrite /y/CNFbB; aw; bw; repeat Ytac0; rewrite /CNFbvo (CNFq_p2).
  by split.
pose ee i := Yo (i = \0c) \0o \1o.
pose cc i := Yo (i = \0c) k j.
move:card1_nz => H.
move: card_lt_12 => lt12.
move: card_lt_02 => lt02.
move: ord_lt_01 BS0 BS1 => l01 bs0 bs1.
have e0: ee \0c = \0o by rewrite /ee; Ytac0.
have e1: ee \1c = \1o by rewrite /ee; Ytac0.
have c0: cc \0c = k by rewrite /cc; Ytac0.
have c1: cc \1c = j by rewrite /cc; Ytac0.
have ax: CNFb_axo ee cc \2c.
  split; first split.
  + apply: ord_le_2omega.
  + move => i lin; rewrite /ee; Ytac h; fprops.
  + by move => i lin; rewrite /cc; Ytac h => //; apply: ord_lt_1omega.
  + move => i iB /card_lt2; rewrite /ee; move: (@succ_nz i) => ss.
    rewrite - succ_zero; case => // si.
    by move: (succ_injective1 (CS_Bnat iB) CS0 si) => iz;Ytac0; Ytac0.
  + move => i lin; rewrite /cc; Ytac h => //.
move: (CNFbB_prop ax BS2); set y := (CNFbB \2c ee cc); move => [ax2 yv].
have py2: P y = \2c by rewrite /y /CNFbB; aw.
move: (CNFB_ax_simp ax2) => [_ ax4].
have eq1: X = CNFBv y.
  rewrite py2 in ax4.
  move: (CNFq_p7 (proj1 ax4) lt12).
  rewrite /X /CNFBv /y /CNFbB !(pr1_pair, pr2_pair) -/CNFbvo => ->.
  rewrite /cantor_mon; bw; repeat Ytac0; rewrite e0 c0 e1 c1.
  by rewrite opowx0 (opowx1 OS_omega) (oprod1l ok).
move:(the_CNF_p0 ox) => [sa sb].
rewrite - sb in eq1; rewrite py2 in ax4.
rewrite /e/c/r /the_CNF_degree.
rewrite (CNFB_unique sa ax2 eq1) py2 - succ_one (cpred_pr1 CS1).
rewrite /CNFbvo (CNFq_p3 (proj1 ax4) lt02) /cantor_mon /y/CNFbB/CNFbvo.
by aw; bw; repeat Ytac0; rewrite e0 opowx0 c0 (oprod1l ok); split.
Qed.

Section NdsStudy1.
Variables (X: fterm) (n:Set).
Hypothesis nB: inc n Bnat.
Hypothesis np: \0c <c n.
Hypothesis ax: nds_tn_ax X n.

Let ee := (the_CNF_degree (X \0c)).

Lemma nds_tn4: ordinalp ee.
Proof. by move:(proj2 ax) => [e ea eb]; rewrite /ee (eb _ np). Qed.

Lemma nds_tn5 i: i<c n -> the_CNF_degree (X i) = ee.
Proof.
by move:(proj2 ax) => [e ea eb] lin; rewrite /ee (eb _ np) (eb _ lin).
Qed.

Let rr:= fun i => CNFbvo (Vg (P (Q (the_CNF (X i)))))
        (Vg (Q (Q (the_CNF (X i)))))
        (cpred (P (the_CNF (X i)))).
Let cc:= fun i => (Vg (Q (Q (the_CNF (X i)))) (cpred (P (the_CNF (X i))))).

Lemma nds_tn6 i: i <c n ->
   [/\ \0o <o cc i, cc i <o omega0, rr i <o omega0 ^o ee &
    X i = omega0 ^o ee *o (cc i) +o rr i].
Proof.
move => lin.
rewrite - (nds_tn5 lin).
have xp:= (proj1 ax i lin).
move:(the_CNF_p0 (proj32_1 xp)) (the_CNF_p2 xp) => [/CNFB_ax_simp [ha hb] hc].
move: ha hb hc; rewrite /cc /rr /ee /the_CNF_degree.
set e := Vg (P (Q (the_CNF (X i)))).
set c := Vg (Q (Q (the_CNF (X i)))).
set ln := (cpred (P (the_CNF (X i)))).
set lm:= (P (the_CNF (X i))).
move => lmB axx Xv [lnB lmv].
have lnm: ln <c lm by move:(card_lt_succ lnB); rewrite - lmv.
split.
+ exact (proj2 axx _ lnm).
+ move: (proj1 axx) =>[_ _ pc _]; exact: (pc _ lnm).
+ apply:(CNFq_pg lnB); rewrite - lmv;exact:(proj1 axx).
+ by rewrite - Xv /CNFBv -/lm lmv /CNFbvo (CNFq_p1 _ _ _ lnB).
Qed.

Lemma nds_tn7 K s: K = emptyset
  -> nds_sc (cardinal K) (fun z => X (nth_elt K z)) s = \0c.
Proof. by move => ->;rewrite cardinal_set0 /nds_sc osum_expansion0. Qed.

Lemma nds_tn8 K s: inc K (powerset (Bint n)) -> inc s (perm_int (cardinal K))
  -> nonempty K
  -> nds_sc (cardinal K) (fun z => X (nth_elt K z)) s =
    omega0 ^o ee *o osum_expansion (fun z => cc (nth_elt K z)) (cardinal K)
    +o rr (nth_elt K (Vf s \0c)).
Proof.
move => /setP_P sb sp nek.
move:(sub_smaller sb); rewrite (card_Bint nB) => ckn.
have ckB:=(BS_le_int ckn nB).
have cknz:= (cardinal_nonemptyset1 nek).
move:(cpred_pr ckB cknz); set k:= cpred _; move => [kB kv].
have ikP: forall i, i<=c k -> (nth_elt K i) <c n.
  move => i /(card_lt_succ_leP kB); rewrite -kv => l1.
  have sKB: sub K Bnat by move => t /sb/(BintP nB) => h; apply(BS_lt_int h nB).
  by move: (nth_set9 (BS_lt_int l1 ckB) sKB l1) => /sb/(BintP nB).
pose Y z := X (nth_elt K z).
pose c z := cc (nth_elt K z).
pose r z := rr (nth_elt K z).
have h2:= nds_tn4.
have h3:(forall i, i <=c k -> \0o <o c i /\ r i <o omega0 ^o ee).
  by move => i /ikP/nds_tn6 [ra _ rb _].
have h4:(forall i, i <=c k -> c i <o omega0).
  by move => i /ikP /nds_tn6 [_ rc _ _].
have lkn: k <c n by apply/(card_le_succ_ltP _ kB); rewrite - kv.
have <-:nds_sc (cardinal K) (fun i => omega0 ^o ee *o c i +o r i) s =
   nds_sc (cardinal K) (fun z => X (nth_elt K z)) s.
  apply:(osum_expansion_exten ckB) => i /(BintP ckB) lin.
  move/(perm_intP): sp => [[[fs _] _] ss ts].
  have: (Vf s i) <c cardinal K by apply/(BintP ckB); Wtac; rewrite ss.
  by rewrite kv; move/(card_lt_succ_leP kB) => /ikP /nds_tn6 [_ _ _ rd].
rewrite kv in sp.
by rewrite kv (nds_p1 kB h2 h3 h4 sp); rewrite /c/r - kv.
Qed.

Lemma nds_tn9 v:
  inc v (nds_tn_S X n) <->
  (v = \0o \/ exists K a, [/\ inc K (powerset (Bint n)), inc a K &
   v =
     omega0 ^o ee *o osum_expansion (fun z => cc (nth_elt K z)) (cardinal K)
    +o rr a]).
Proof.
split.
  move/setUf_P => [K ka /funI_P [s sp sv]].
  case:(emptyset_dichot K) => ke.
    by rewrite sv ke cardinal_set0/nds_sc osum_expansion0; left.
  right; exists K,(nth_elt K (Vf s \0c)).
  move/(perm_intP): (sp) => [[[fs _] _] ss ts].
  have h:inc (nth_elt K (Vf s \0c)) K.
    move/setP_P: ka => ka.
    have sKB: sub K Bnat by move => t /ka/(BintP nB) => h;apply(BS_lt_int h nB).
    move:(sub_smaller ka); rewrite (card_Bint nB) => ckn.
    have ckB:=(BS_le_int ckn nB).
    have cknz:= (cardinal_nonemptyset1 ke).
    have zi: inc \0c (Bint (cardinal K)).
      apply /(BintP ckB); split; [ apply: czero_least; fprops | fprops].
    have l1: (Vf s \0c) <c cardinal K by apply/(BintP ckB); Wtac; rewrite ss.
    by move:(nth_set7 (BS_lt_int l1 ckB) sKB l1) => [/setC_P []].
  by split => //; rewrite sv - (nds_tn8 ka sp ke).
case => vv.
   apply/setUf_P; exists emptyset; first by apply: setP_0i.
   apply/funI_P; exists (identity (Bint (cardinal emptyset))).
      apply:perm_int_id.
   by rewrite cardinal_set0 /nds_sc osum_expansion0.
move:vv=> [K [a [Ks1 aK ->]]]; apply/setUf_P; exists K => //.
have neK: nonempty K by ex_tac.
move/setP_P: (Ks1) => ka.
have sKB: sub K Bnat by move => t /ka/(BintP nB) => h;apply(BS_lt_int h nB).
move:(sub_smaller ka); rewrite (card_Bint nB) => ckn.
have cknz:= (cardinal_nonemptyset1 neK).
have ckB:=(BS_le_int ckn nB).
move:(cpred_pr ckB cknz); set k:= cpred _; move => [kB kv].
have fsk: finite_set K by apply/BnatP.
move:(nth_set_10 sKB fsk aK) => [i il1 iv].
move: (permutation_exists1 ckB il1) => [f fp fiv].
rewrite -fiv in iv.
by apply/funI_P;ex_tac; rewrite (nds_tn8 Ks1 fp neK) - iv.
Qed.

Lemma nds_p3 a K:inc K (powerset (Bint n)) -> inc a K ->
  omega0 ^o ee *o osum_expansion (fun z => cc (nth_elt K z)) (cardinal K)
    +o rr a =
  omega0 ^o ee *o card_sumb (K -s1 a) cc +o X a.
Proof.
move => pa pb.
have h1:(forall i, i <c n -> inc (cc i) Bnat).
  by move => i /nds_tn6 [_ /(ord_ltP OS_omega) h _ _].
rewrite (nds_p2 nB h1 pa).
move: (setC1_K pb); set K1:= K -s1 a => Kv.
move/setP_P:pa => Kb.
have ss1:= (@sub_setC K (singleton a)).
have fsK:=(sub_finite_set Kb (finite_Bint n)).
have h2:=(sub_finite_set ss1 fsK).
have skB: inc (card_sumb K1 cc) Bnat.
  apply:finite_sum_finite; hnf; rewrite/allf;bw;split => //.
  move => t tk1; bw; apply: h1;apply /(BintP nB); apply: (Kb _ (ss1 _ tk1)).
have ak1:~ inc a K1 by move/setC1_P=> [ _ ].
move /(BintP nB): (Kb _ pb) =>/nds_tn6 [_ _ /proj31_1 o4 r2].
have ccaB: inc (cc a) Bnat by apply: h1; apply /(BintP nB);apply: Kb.
rewrite -{1} Kv (csumA_setU1 _ ak1) - (osum2_2int skB ccaB).
have o1:=(OS_pow OS_omega nds_tn4).
move: (Bnat_oset ccaB) (Bnat_oset skB) => o2 o3.
by rewrite (osum_prodD) // - (osumA (OS_prod2 o1 o3) (OS_prod2 o1 o2) o4) r2.
Qed.

Lemma nds_tn10: (nds_tn_S X n) =
  unionf (Bint n) (fun a => fun_image (powerset ((Bint n) -s1 a))
   (fun K => omega0 ^o ee *o (card_sumb K cc) +o X a)) +s1 \0c.
Proof.
set_extens v.
  case /nds_tn9;[ move ->; fprops | move => [K [a [kp ak ->]]] ].
  apply/setU1_P; left; apply /setUf_P.
  move/setP_P:(kp) => kb;move:(kb _ ak) => aN;ex_tac; apply /funI_P.
  exists (K -s1 a).
    by apply/setP_P => t/setC1_P [ha hb]; apply/setC1_P; split=> //; apply:kb.
  by rewrite nds_p3.
case/setU1_P => h1; apply/nds_tn9; [right | by left].
move/setUf_P: h1 => [a aB /funI_P[K /setP_P Kb ->]].
have nk1: ~ (inc a K) by move /Kb => /setC1_P[].
have eq1:= setU1_K nk1.
have ha: inc (K +s1 a) (powerset (Bint n)).
   apply /setP_P => t/setU1_P; case; [by move/Kb => /setC1_P[] | by move ->].
have hb:inc a (K +s1 a) by fprops.
by exists (K +s1 a),a; split => //; rewrite (nds_p3 ha hb) eq1.
Qed.

Lemma nds_tn11: (nds_tn_C X n) <=c ndstnC n.
Proof.
rewrite /nds_tn_C nds_tn10/ndstnC.
set S := unionf _ _.
suff h: cardinal S <=c (n *c \2c ^c cpred n).
  have w:cardinalp (n *c \2c ^c cpred n) by fprops.
  have w1:= (card_le_succ0 w).
  case: (inc_or_not \0c S) => ha; first by rewrite (setU1_eq ha); co_tac.
  by rewrite (card_succ_pr ha); apply /(card_le_succ_succP (CS_cardinal S) w).
rewrite /S; set F:= (fun a : Set => _).
move:(cpred_pr nB (nesym (proj2 np))) => [pnB pnv].
move:(csum_pr1_bis (Bint n) F).
set g1:= (Lg (Bint n) (fun a => cardinal (Vg (Lg (Bint n) F) a))).
have <-: card_sum g1 = card_sumb (Bint n) (fun a : Set => cardinal (F a)).
  rewrite /card_sumb;apply:f_equal;apply:Lg_exten => t tx; bw.
set g2 := cst_graph (Bint n) (\2c ^c cpred n).
have sd: domain g1 = domain g2 by rewrite /g1/g2; bw.
suff le1:forall x, inc x (domain g1) -> Vg g1 x <=c Vg g2 x.
  move:(csum_increasing sd le1).
  rewrite csum_of_same cprodC - cprod2_pr2a (card_Bint nB).
  move => hb ha ; exact:(card_leT ha hb).
rewrite /g1 /g2; bw => a abn; bw.
have ->: \2c ^c cpred n = cardinal (powerset (Bint n -s1 a)).
  move: (card_succ_pr2 abn); rewrite (card_Bint nB) => eq1.
  rewrite card_setP - (cpow_prb _ ((Bint n -s1 a))); apply: f_equal.
  apply:succ_injective1; fprops; ue.
apply: fun_image_smaller.
Qed.

Lemma nds_tn11_ex:
  (forall i, X i = omega0 *o (\2c ^c i) +o i) ->
  (nds_tn_S X n) =
  unionf (Bint n) (fun a => fun_image (powerset ((Bint n) -s1 a))
   (fun K => omega0 *o (card_sumb K (fun i => (\2c ^c i))) +o X a)) +s1 \0c.
Proof.
move => h.
rewrite nds_tn10.
have ha: forall i, inc i Bnat -> inc (\2c ^c i) Bnat.
  move => i; apply:(BS_pow BS2).
have hb: forall i, inc i Bnat -> \0c <c (\2c ^c i).
  by move => i ib; split;[ fprops |apply: nesym;apply: cpow2_nz].
have ->: ee = \1o.
  move:(proj31 (proj2 (the_CNF_omega_kj (ha _ BS0) BS0 (hb _ BS0)))).
  by rewrite - (h \0c).
apply:f_equal2; last by exact.
rewrite (opowx1 OS_omega).
have aux: forall y, sub y Bnat ->
  card_sumb y [eta card_pow \2c] = card_sumb y cc.
  move => y yb; rewrite /card_sumb /card_sum; apply:f_equal; apply:f_equal.
  apply:Lg_exten => t /yb yB.
  move: (proj32 (proj2 (the_CNF_omega_kj (ha _ yB) yB (hb _ yB)))).
  by rewrite - (h t).
have H2: forall y a, inc y (powerset (Bint n -s1 a)) -> sub y Bnat.
  by move => y a /setP_P hy t /hy /setC1_P [/Bint_S1 uu _].
set F1 := fun a: Set => _; set F2 := fun a: Set => _.
suff r1: forall a, inc a (Bint n) -> F1 a = F2 a.
  set_extens t => /setUf_P [y ya yb]; apply/setUf_P; exists y;
   [exact |by rewrite - (r1 _ ya) | exact | by rewrite (r1 _ ya)].
move => a ab; set_extens t; move => /funI_P [y ya ->]; apply/funI_P.
  exists y; [exact | by rewrite (aux _ (H2 _ _ ya))].
 exists y; [exact | by rewrite (aux _ (H2 _ _ ya))].
Qed.

End NdsStudy1.

Definition sumpow2 K := card_sumb K (fun z => \2c ^c z).

Lemma omega_monom_inj a b c d:
   inc a Bnat -> inc b Bnat -> inc c Bnat -> inc d Bnat
  -> omega0 *o a +o b = omega0 *o c +o d -> (a = c /\ b = d).
Proof.
move => aB bB cB dB eq1.
have aux: forall u v, inc u Bnat -> inc v Bnat ->inc (omega0 *o u +o v) Bnat
   -> u = \0c.
  move => u v uB vB h; ex_middle h1.
  have h2:= (ozero_least (Bnat_oset uB)).
  have h3: \0o <o u by split; [apply: h2| apply:nesym].
  have l1:=(oprod_Mle1 OS_omega h3).
  move:(ord_leT l1 (osum_Mle0 (proj32 l1) (Bnat_oset vB))) => l2.
  move/(ord_ltP OS_omega): h => l3; ord_tac.
case: (equal_or_not a \0c) => az.
  move: eq1; rewrite az oprod0r (osum0l (Bnat_oset bB)) => eq1.
  rewrite eq1 in bB.
  by rewrite eq1 (aux _ _ cB dB bB) oprod0r (osum0l (Bnat_oset dB)).
case: (equal_or_not c \0c) => cz.
  move: eq1; rewrite cz oprod0r (osum0l (Bnat_oset dB)) => eq1.
  case: az;rewrite - eq1 in dB; exact:(aux _ _ aB bB dB).
have ap: \0c <c a by split; fprops.
have cp: \0c <c c by split; fprops.
move:(the_CNF_omega_kj aB bB ap) => [_ [_ e1 e2]].
move:(the_CNF_omega_kj cB dB cp) => [_ [_ e3 e4]].
by rewrite eq1 in e1 e2; rewrite e1 in e3; rewrite e2 in e4.
Qed.

Lemma sumpow2_a K: finite_set K -> sub K Bnat -> inc (sumpow2 K) Bnat.
Proof.
move => ha hb; apply:finite_sum_finite; split; aw; bw.
hnf; bw => x xk; bw; fprops.
Qed.

Lemma sumpow2_b n a K:
  inc n Bnat -> inc K (powerset (Bint n -s1 a)) -> inc (sumpow2 K) Bnat.
Proof.
move => nB /setP_P h1; move:(sub_trans h1 (@sub_setC _ _)) => h2.
have h3:= (sub_trans h2 (@Bint_S1 n)).
exact (sumpow2_a (sub_finite_set h2 (finite_Bint n)) h3).
Qed.

Lemma sumpow2_c a K: ~ (inc a K) ->
  sumpow2 (K+s1 a) = sumpow2 K +c (\2c ^c a).
Proof. by move => naK; rewrite /sumpow2 (csumA_setU1 _ naK). Qed.

Lemma sumpow2_d a K: inc a K ->
  sumpow2 K = sumpow2 (K -s1 a) +c (\2c ^c a).
Proof.
by move => aK; rewrite -{1} (setC1_K aK) sumpow2_c // => /setC1_P [].
Qed.

Lemma sumpow2_e n a K (X := fun i => omega0 *o (\2c ^c i) +o i):
  inc n Bnat -> inc a (Bint n) ->
  inc K (powerset (Bint n -s1 a)) ->
  omega0 *o (sumpow2 K) +o X a = omega0 *o (sumpow2 (K +s1 a)) +o a
  /\ (inc (sumpow2 (K +s1 a)) Bnat).
Proof.
move => nB ak KP.
have aB := (@Bint_S1 n a ak).
have haa: inc (\2c ^c a) Bnat by fprops.
have naK: ~ inc a K by move/