Library sset13

Theory of Sets : Ordinals

Copyright INRIA (2009-2013) Apics, Marelle Team (Jose Grimm).


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

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

Module Ordinals3.

Cantor normal form

Any ordinal is uniquely a sum of decreasing powers of omega

Definition CNF_graph f :=
 fgraph f /\ (exists2 n, inc n Bnat & domain f = Bint n).

Lemma CNF_domain X: CNF_graph X ->
   domain X = Bint (cardinal (domain X)).
Proof. move => [_ [m mB mv]]; rewrite mv; bw. Qed.

Lemma CNF_domain1 X: CNF_graph X -> inc (cardinal (domain X)) Bnat.
Proof. move => [_ [m mB ->]]; bw. Qed.

Lemma CNF_domain2 X i: CNF_graph X -> inc i (domain X) -> inc i Bnat.
Proof. by move => [_ [m mB ->]] /Bint_S1. Qed.

Lemma CNF_domainP X: CNF_graph X ->
  forall i, (inc i (domain X) <-> i <c (cardinal (domain X))).
Proof.
move=> h; rewrite {1} (CNF_domain h)=> i; bw => //.
have aux: inc (cardinal (domain X)) Bnat by apply: CNF_domain1.
exact: (BintP aux).
Qed.

Definition CNFrv0 f n := osum_expansion (fun i => (omega0 ^o (f i))) n.
Definition CNFrv f := CNFrv0 (Vg f) (cardinal (domain f)).
Definition CNFr_ax0 f n:=
  ord_below_n f n
  /\ (forall i, inc i Bnat -> (succ i) <c n -> (f i) <=o (f (succ i))).

Definition CNFr_ax f:=
  [/\ CNF_graph f,
  (allf f ordinalp) &
  (forall i, inc i (domain f) -> inc (succ i) (domain f) ->
     (Vg f i) <=o (Vg f (succ i)))].

Lemma CNFr_ax_p1 f n: inc n Bnat -> CNFr_ax0 f n ->
  CNFr_ax (Lg (Bint n) f).
Proof.
move => nB [ax1 ax2].
split; first by split; [ fprops | exists n; bw].
  by hnf; bw => x xd; bw; apply: ax1; apply /(BintP nB).
bw; move => i i1 i2; bw.
apply: ax2; [exact: (Bint_S1 i1) | by apply /(BintP nB)].
Qed.

Lemma CNFr_ax_p2 f: CNFr_ax f -> CNFr_ax0 (Vg f) (cardinal(domain f)).
Proof.
move => [ax1 ax2 ax3].
split; first by move => i /(CNF_domainP ax1) idf; apply: ax2.
move => i ib si.
move: (card_le_ltT (card_le_succ ib) si) => /(CNF_domainP ax1) id1.
by apply: ax3 => //; apply /(CNF_domainP ax1).
Qed.

Lemma CNFr_ax_p3 f n: inc n Bnat -> CNFr_ax0 f (succ n) -> CNFr_ax0 f n.
Proof.
move => nB [ax1 ax2]; move: (card_lt_succ nB) => pa;split=> //.
  move=> i lin; apply: ax1; co_tac.
move => i iB si; apply: ax2 => //; co_tac.
Qed.

Lemma CNFr_p1 f n: inc n Bnat ->
  CNFrv (Lg (Bint n) f) = CNFrv0 f n.
Proof.
move => nB; rewrite /CNFrv Lg_domain (card_Bint nB).
by apply: (osum_expansion_exten nB) => i lin; bw; apply/(BintP nB).
Qed.

Lemma OS_CNFr0 f n: inc n Bnat -> CNFr_ax0 f n -> ordinalp (CNFrv0 f n).
Proof.
move => nB [ax1 ax2];apply: (OS_osum_expansion nB) => i lin.
apply: (OS_pow OS_omega (ax1 _ lin)).
Qed.

Lemma CNFr_p2 f n: inc n Bnat -> CNFr_ax0 f (succ n) ->
  (omega0 ^o (f n)) <=o CNFrv0 f (succ n).
Proof.
move => nB ax; move:(CNFr_ax_p3 nB ax) => axr.
rewrite /CNFrv0 (osum_expansion_succ _ nB).
have lt1:= (card_lt_succ nB).
apply: osum_Mle0; last by apply: (OS_CNFr0 nB axr).
by apply: (OS_pow OS_omega (proj1 ax _ (card_lt_succ nB))).
Qed.

Lemma CNFr_p3 f n i:
  inc n Bnat -> CNFr_ax0 f n -> i <c n ->
  omega0 ^o (f i) <=o CNFrv0 f n.
Proof.
move => nB ax lin.
case (equal_or_not n \0c) => nz.
  by move: lin; rewrite nz=> /card_lt0.
move: (cpred_pr nB nz) => [pB pv]. rewrite pv in ax.
move: (CNFr_p2 pB ax); rewrite - pv => e1.
have rec: forall j, \0c <=c j -> j <c cpred n ->
     omega0 ^o f (succ j) <=o CNFrv0 f n -> omega0 ^o f j <=o CNFrv0 f n.
  move => j oj jln le1.
  have pa := (BS_lt_int jln pB).
  have pb: succ j <c succ (cpred n).
    by apply/(card_lt_succ_leP pB); apply /(card_le_succ_ltP _ pa).
  move: (opow_Momega_le (proj2 ax j pa pb)) => l2; ord_tac.
have ip: \0c <=c i by apply: czero_least; co_tac.
have ipn:i <=c cpred n by apply/(card_lt_succ_leP pB); ue.
exact: (cardinal_c_induction4 BS0 pB e1 rec ip ipn).
Qed.

Lemma CNFr_p4 f n m: inc n Bnat -> CNFr_ax0 f (succ n) ->
  f n <o m -> CNFrv0 f (succ n) <o omega0 ^o m.
Proof.
move => nB ax lt1.
suff: CNFrv0 f (succ n) <=o (omega0 ^o (f n) *o (succ n)).
  have sno: succ n <o omega0.
    apply /ord_ltP; [ apply: OS_omega | apply: BS_succ; fprops ].
  move => h; apply: (ord_le_ltT h).
  move: (lt1) => [[cv _ _ ] _].
  move: (omega_pow_pos cv) => op.
  have: omega0 ^o f n *o succ n <o omega0 ^o f n *o omega0.
    by apply: oprod_Meqlt.
  rewrite - (opow_succ OS_omega cv) => h1; apply: (ord_lt_leT h1).
  by apply: opow_Momega_le; apply /ord_succ_ltP.
set p := f n.
have: f n <=o p by rewrite /p; apply: ord_leR; ord_tac.
move: p; clear lt1 m.
move: n nB f ax; apply: cardinal_c_induction.
  move => f ax p hp.
  move:(OS_pow OS_omega (proj32 hp)) (OS_pow OS_omega (proj31 hp)) => ha hb.
  rewrite succ_zero (oprod1r ha) /CNFrv0 osum_expansion1 //.
  by apply:opow_Momega_le.
move => n nB Hrec f ax m le1.
have snB:=(BS_succ nB).
have le2:=(opow_Momega_le le1).
have h := (ord_leT (proj2 ax n nB (card_lt_succ snB)) le1).
have le3:=(Hrec f (CNFr_ax_p3 snB ax) m h).
move:(osum_Mlele le2 le3).
rewrite {1}/CNFrv0 -(osum_expansion_succ (fun i => omega0 ^o f i) snB).
have osn: ordinalp (succ n) by apply: OS_cardinal; fprops.
rewrite (osum_x_xy (OS_pow OS_omega (proj32 le1)) osn).
by rewrite (osum2_2int BS1 snB) csumC - (Bsucc_rw snB).
Qed.

Lemma CNFr_p5 f: CNFrv0 f \0c = \0o.
Proof. by rewrite /CNFrv0 osum_expansion0. Qed.

Lemma CNFr_p6 f n: inc n Bnat -> CNFr_ax0 f n -> n <> \0c ->
    CNFrv0 f n <> \0o.
Proof.
move => nB ax nz rz.
move: (cpred_pr nB nz) => [sa sb].
rewrite sb in ax rz.
move:(CNFr_p2 sa ax). rewrite rz.
move: (omega_pow_pos (proj1 ax _ (card_lt_succ sa))) => l1 l2; ord_tac.
Qed.

Lemma CNFr_unique1 f g n m: CNFr_ax0 f n -> CNFr_ax0 g m ->
   inc n Bnat -> inc m Bnat -> CNFrv0 f n = CNFrv0 g m ->
   (n = m /\ forall i, i <c n -> f i = g i).
Proof.
move => p1 p2 p3 p4; move: n p3 m p1 p2 p4; apply: cardinal_c_induction.
  move => m af ag mB sv; split; last by move => i /card_lt0 h; case h.
  symmetry;ex_middle bad.
  by move: (CNFr_p6 mB ag bad); rewrite - sv CNFr_p5; case.
move => n nB Hrec m af ag mB sv.
case: (equal_or_not m \0c) => mz.
  by move: (CNFr_p6 (BS_succ nB) af (@succ_nz n)); rewrite sv mz CNFr_p5; case.
move: (cpred_pr mB mz); set m':= (cpred m); move => [m'B mv].
rewrite mv in ag sv.
move: (CNFr_ax_p3 nB af) (CNFr_ax_p3 m'B ag) => ax1 ax2.
move: sv (CNFr_p4 nB af (m:= g m')) (CNFr_p4 m'B ag (m:= f n)).
move:(CNFr_p2 nB af) (CNFr_p2 m'B ag).
rewrite /CNFrv0 (osum_expansion_succ _ nB)(osum_expansion_succ _ m'B).
rewrite -/(CNFrv0 _ _) -/(CNFrv0 _ _).
move => le1 le2 eq1 lt1 lt2.
move: (card_lt_succ nB) (card_lt_succ m'B) => ns1 ns2.
case (ord_le_to_ell (proj1 af _ ns1) (proj1 ag _ ns2)).
+ move => eq2.
  rewrite eq2 in eq1.
  move: (osum2_simpl (OS_CNFr0 nB ax1) (OS_CNFr0 m'B ax2) (proj31 le2) eq1).
  move / (Hrec m' ax1 ax2 m'B)=> [ra rb].
  rewrite mv -ra; split; [ reflexivity | move => i /(card_lt_succ_leP nB) li].
  case (equal_or_not i n); first by move => ->; rewrite eq2 ra.
  by move => ni; apply:rb; split.
+ move /lt1; rewrite eq1 => ll; ord_tac.
+ move /lt2; rewrite - eq1 => ll; ord_tac.
Qed.

Lemma CNFr_unique f g:
  CNFr_ax f -> CNFr_ax g -> CNFrv f = CNFrv g -> f = g.
Proof.
move => af ag; rewrite /CNFrv.
move:(af)(ag) => [af1 _ _ ][ag1 _ _].
move: (CNF_domain1 af1) (CNF_domain1 ag1) (CNF_domain af1) (CNF_domain ag1).
move: (CNFr_ax_p2 af) (CNFr_ax_p2 ag).
set n := (cardinal (domain f)); set m := (cardinal (domain g)).
move => ax1 ax2 nB mB d1 d2 sv;move:(CNFr_unique1 ax1 ax2 nB mB sv)=> [sa sb].
move: (af1) (ag1) => [fgf _] [fg _].
apply: fgraph_exten; [done | done | by rewrite d1 d2 sa | move => i].
rewrite d1; move/(BintP nB); apply: sb.
Qed.

Lemma CNFr_exists x: ordinalp x ->
  exists2 f, CNFr_ax f & x = CNFrv f.
Proof.
move => ox.
suff: exists f n, [/\ inc n Bnat, CNFr_ax0 f n & x = CNFrv0 f n].
  move => [f [n [pa pb pc]]].
  move: (CNFr_ax_p1 pa pb) (CNFr_p1 f pa); rewrite - pc => pd pe.
  by exists (Lg (Bint n) f); [ exact | symmetry].
pose p x := exists f n, [/\ inc n Bnat, CNFr_ax0 f n & x = CNFrv0 f n].
apply: (least_ordinal2 (p:=p)) ox => y oy p2.
case: (ord_zero_dichot oy) => yp.
  exists (@id Set), \0c; split; [ fprops | | by rewrite CNFr_p5 yp].
  split => i; [ move /card_lt0; case | move => _ /card_lt0; case].
move: (ord_ext_div_exists ord_le_2omega yp)
   =>[e1 [c1 [rm [oe1 oc1 or [eq1 lt1 lt2 lt3]]]]].
move: (ord_rev_pred lt3); set c2 := (c1 -o \1o); move => [oc2 eql].
have eql2: c1 = c2 +o \1o.
  move: (osum_M0le OS1 oc2);rewrite - eql => h; move: (ord_le_ltT h lt2) => aa.
  have c2B: inc c2 Bnat by rewrite - /ord_ltP //; ord_tac.
  by move: eql; rewrite (osum2_2int BS1 c2B) csumC - (osum2_2int c2B BS1).
set q := (omega0 ^o e1); set rm1 := ((q *o c2) +o rm).
have oq: ordinalp q by ord_tac.
have op2: ordinalp (q *o c2) by fprops.
have orm1: ordinalp rm1 by rewrite /rm1; fprops.
move: OS_omega OS1 => oo o1.
have yv1: y = q +o rm1 by rewrite eq1 eql osum_prodD // oprod1r // /rm1 osumA.
have pv2: q *o c1 = (q *o c2) +o q by rewrite eql2 osum_prodD // oprod1r //.
have yv2: y = (q *o c2) +o (q +o rm) by rewrite eq1 pv2 osumA //.
have rmy: rm1 <o y.
  split; first by rewrite yv1; apply: osum_M0le => //.
  rewrite /rm1 yv2 => eq3.
  move: (osum_Mle0 oq or);rewrite - (osum2_simpl or (OS_sum2 oq or) op2 eq3).
  move => h; ord_tac.
move:(p2 _ rmy) => [f [n [nB p4 p5]]].
have snb:= (BS_succ nB).
pose g z:= (Yo (z = n) e1 (f z)).
have yv3: y = CNFrv0 g (succ n).
  rewrite /CNFrv0 (osum_expansion_succ _ nB) /g yv1; Ytac0; congr (ord_sum2).
  by rewrite p5;apply: (osum_expansion_exten nB) => i [_ lin]; Ytac0.
have ax2:CNFr_ax0 g (succ n).
  split.
    move => i; rewrite /g; Ytac ein => //.
    by move/(card_lt_succ_leP nB) => lin; apply:(proj1 p4).
  move => i iB h; rewrite /g.
  move/(card_lt_succ_leP nB): h => sin.
  Ytac ein; first by move: (card_lt_succ nB); rewrite - {2} ein => l1; co_tac.
  Ytac sein; last by apply:(proj2 p4).
  move: (card_lt_succ iB); rewrite sein => lin.
  case:(ord_le_to_el (proj1 p4 _ lin) oe1)=> // /ord_succ_ltP/opow_Momega_le sb.
  have aux: omega0 ^o (f i) <=o rm1 by rewrite p5;apply:(CNFr_p3 nB p4 lin).
  move: (osum_Meqlt lt1 op2); rewrite - pv2 => lt6.
  move:(oprod_Meqle (proj1 lt2) oq) => le5.
  move: (ord_lt_leT lt6 le5); rewrite /q - (opow_succ oo oe1) -/rm1 => sc.
  move: (ord_le_ltT aux sc) => sa; ord_tac.
by exists g,(succ n).
Qed.

Definition ord_negl a b := a +o b = b.
Notation "x <<o y" := (ord_negl x y) (at level 60).

Lemma ord_negl_lt a b: ordinalp a -> ordinalp b ->
  a <<o b -> ((a = \0o /\ b = \0o) \/ (a <o b)).
Proof.
rewrite /ord_negl;move=> oa ob abz.
case: (equal_or_not b \0o) => bz.
  by move: abz; rewrite bz (osum0r oa); left.
right; split; first by rewrite -abz; apply: osum_Mle0.
dneg ab; rewrite ab in abz; apply: (osum_a_ab ob ob abz).
Qed.

Lemma ord_negl_sum a b c: ordinalp a -> ordinalp b -> ordinalp c ->
  a <<o b -> a <<o (b +o c).
Proof.
by rewrite /ord_negl => oa ob oc h; rewrite osumA // h.
Qed.

Lemma ord_negl_prod a b c: ordinalp a -> ordinalp b ->
   \0o <o c -> a <<o b -> a <<o (b *o c).
Proof.
move=> oa ob cnz lab.
move: (ord_rev_pred cnz) => [oy ->].
rewrite (osum_prodD OS1 oy ob) (oprod1r ob).
by apply: ord_negl_sum => //; fprops.
Qed.

Lemma ord_negl_sum1 a b c:
  ordinalp a -> ordinalp b -> ordinalp c ->
  a <<o c -> b <<o c -> (a +o b) <<o c.
Proof. rewrite /ord_negl => oa ob oc p1 p2; by rewrite - osumA // p2 p1. Qed.

Lemma ord_negl_sum2 a b c:
  ordinalp a -> ordinalp b -> ordinalp c ->
  (a +o b) <<o c -> (a <<o c /\ b <<o c).
Proof.
rewrite /ord_negl => oa ob oc.
rewrite - (osumA oa ob oc) => h.
suff: b +o c = c by move => h1; rewrite -{2} h h1.
move: (osum_M0le ob oc) => sa.
move: (osum_M0le oa (OS_sum2 ob oc)); rewrite h => h2; ord_tac.
Qed.

Lemma ord_negl_sum3 a b c:
  ordinalp c -> a <=o b -> b <<o c -> a <<o c.
Proof.
move => oc h1; move: (h1) => [oa _ _].
by move: (odiff_pr h1) => [od -> /(ord_negl_sum2 oa od oc) []].
Qed.

Lemma ord_neg_sum4 a b: ordinalp a -> ordinalp b ->
  a <<o (a +o b) -> a <<o b.
Proof. move => oa ob; apply: osum2_simpl; fprops. Qed.

Lemma ord_negl_p1 b: b <o omega0 -> b <<o omega0.
Proof.
move : OS_omega => oo bo.
exact: (indecomp_prop1 indecomp_omega bo).
Qed.

Lemma ord_negl_p2 b e:
  b <o omega0 -> \0o <o e ->
  b <<o (omega0 ^o e).
Proof.
move=> bo ne0.
move: OS_omega OS1 => oo o1.
move: (ord_rev_pred ne0) => [oy ->].
have ob: ordinalp b by ord_tac.
have ooy: ordinalp (omega0 ^o (e -o \1o)) by fprops.
rewrite (opow_sum oo o1 oy) (opowx1 oo).
by apply: ord_negl_prod => //;[ apply: omega_pow_pos | by apply: ord_negl_p1].
Qed.

Lemma ord_negl_p3 b e d:
  b <o omega0 -> \0o <o e -> \0o <o d ->
  b <<o ((omega0 ^o e) *o d).
Proof.
move=> bo ne0 nd0.
have ob: ordinalp b by ord_tac.
have oe: ordinalp e by ord_tac.
move: (ord_negl_p2 bo ne0) => aux.
apply: ord_negl_prod => //; fprops.
Qed.

Lemma ord_negl_p4 a b:
  a <o b -> (omega0 ^o a) <<o (omega0 ^o b).
Proof.
move: OS_omega => ox ltab.
have leac: a <=o b by move: ltab => [? _].
move: (odiff_pr leac) => [odi pa].
move: (odiff_pos ltab) => dp.
have ora: ordinalp a by ord_tac.
have oa1: ordinalp (omega0 ^o a) by fprops.
have oa2: ordinalp (omega0 ^o (b -o a)) by fprops.
rewrite pa (opow_sum ox ora odi) /ord_negl osum_x_xy //.
congr (_ *o _); apply: ord_negl_p2 => //; apply: ord_lt_1omega.
Qed.

Lemma ord_negl_p5 e c e' c':
  c <o omega0 -> e <o e' -> \0o <o c' ->
  ((omega0 ^o e) *o c) <<o ((omega0 ^o e') *o c').
Proof.
move=> ltco ltee' cnz /=.
move: OS_omega => ox.
have leee': e <=o e' by move: ltee' => [? _].
move: (odiff_pr leee') => [odi pa].
have orc: ordinalp e by ord_tac.
have ore: ordinalp c by ord_tac.
have oc': ordinalp c' by ord_tac.
set x:= omega0.
have oa1: ordinalp (x ^o e) by fprops.
have oa2: ordinalp (x ^o (e' -o e)) by fprops.
have oa3: ordinalp ((x ^o (e' -o e)) *o c') by fprops.
have ->: ((x ^o e') *o c') = (x ^o e) *o ( (x ^o (e' -o e)) *o c').
  rewrite oprodA // - (opow_sum ox orc odi) - pa //.
rewrite /ord_negl - osum_prodD //.
by congr (_ *o _); apply: ord_negl_p3 => //; apply: odiff_pos.
Qed.

Lemma ord_negl_p6 e f n:
  inc n Bnat -> CNFr_ax0 f (succ n) ->
  e <o (f n) -> (omega0 ^o e) <<o (CNFrv0 f (succ n)).
Proof.
move: OS_omega => oo nB h ef.
have oe: ordinalp e by ord_tac.
have o1: ordinalp (omega0 ^o e) by fprops.
have o2: ordinalp (omega0 ^o (f n)) by apply:OS_pow => //; ord_tac.
have lt1:= (ord_negl_p4 ef).
rewrite /CNFrv0 (osum_expansion_succ _ nB); apply: ord_negl_sum => //.
exact:(OS_CNFr0 nB (CNFr_ax_p3 nB h)).
Qed.

Lemma ord_negl_pg f n g m:
  inc n Bnat -> CNFr_ax0 f (succ n) ->
  inc m Bnat -> CNFr_ax0 g (succ m) ->
  (g m <o f n <-> CNFrv0 g (succ m) <<o CNFrv0 f (succ n)).
Proof.
move=> nB cf mB cg; split.
  move: m mB cg;apply: cardinal_c_induction.
    rewrite succ_zero {1} /CNFrv0=> ax1 lt1.
    have h:= (OS_pow OS_omega(proj31_1 lt1)).
    rewrite (osum_expansion1)//; exact:(ord_negl_p6 nB cf lt1).
  move => m mB Hrec cdg ltspd.
  move: OS_omega (BS_succ mB) => oo smB.
  rewrite {1} /CNFrv0 (osum_expansion_succ _ smB).
  have ax2:= (CNFr_ax_p3 smB cdg).
  have o1:= (OS_pow oo (proj1 cdg _ (card_lt_succ smB))).
  apply:(ord_negl_sum1 o1 (OS_CNFr0 smB ax2) (OS_CNFr0 (BS_succ nB) cf)).
  apply: (ord_negl_p6 nB cf ltspd).
  apply: Hrec => //.
  move: (proj2 cdg m mB (card_lt_succ smB)) => la; ord_tac.
move: (CNFr_p2 nB cf) => sa.
rewrite {1}/CNFrv0 (osum_expansion_succ _ mB) => t2.
have ax2:= (CNFr_ax_p3 mB cg).
have o0:= (proj1 cg _ (card_lt_succ mB)).
have o2:= (proj1 cf _ (card_lt_succ nB)).
have o1:= (OS_pow OS_omega o0).
move: (proj1 (ord_negl_sum2 o1 (OS_CNFr0 mB ax2) (proj32 sa) t2)) => le1 {t2}.
case:(ord_negl_lt o1 (proj32 sa) le1);[ move => [] | move => lt0].
   by move:(omega_pow_nz o0).
case:(ord_le_to_ell o0 o2) => // le2; last first.
  move:(CNFr_p4 nB cf le2) => [h _]; ord_tac.
rewrite le2 in le1 lt0; apply: False_ind.
move: nB cf le1 lt0; clear; move => nb; move: n nb.
apply: cardinal_c_induction.
  rewrite succ_zero => h1 _.
  have ha:= (OS_pow OS_omega (proj1 h1 \0o card_lt_01)).
  by rewrite /CNFrv0 osum_expansion1 //; move => [].
move => n nB Hrec ax1.
have snB:= (BS_succ nB).
rewrite /CNFrv0 (osum_expansion_succ _ snB) -/(CNFrv0 _ _) => ha hb.
have ax2:= (CNFr_ax_p3 snB ax1).
have o0:= (proj1 ax1 _ (card_lt_succ snB)).
have o1:= (OS_pow OS_omega o0).
have o3 := (OS_CNFr0 snB ax2).
have hc :=(ord_neg_sum4 o1 o3 ha).
have le0:= (proj2 ax1 _ nB (card_lt_succ snB)).
have le1:= (opow_Momega_le le0).
move: (ord_negl_sum3 o3 le1 hc) => pra.
case: (ord_negl_lt (proj31 le1) o3 pra); last by move /(Hrec ax2 pra).
by move:(omega_pow_nz (proj1 ax2 _ (card_lt_succ nB))) => h1 [].
Qed.

Lemma cantor_of_limit x: limit_ordinal x ->
  exists a n, [/\ ordinalp a, ordinalp n, n <> \0o,
   x = a +o (omega0 ^o n)
   & (a = \0o \/
      [/\ limit_ordinal a, (omega0 ^o n) <=o a
       & cardinal x = cardinal a])].
Proof.
move/limit_ordinal_P3 => [xnz lx].
move: (CNFr_exists (proj32_1 xnz)) => [X ax xv].
move: (CNFr_ax_p2 ax) (CNF_domain1 (proj31 ax)); set n := cardinal _.
move => ax1 nB.
case: (equal_or_not n \0c) => nz.
 by case: xnz; rewrite xv /CNFrv /CNFrv0 -/n nz osum_expansion0.
have cn1: \1c <=c n by apply: card_ge1; fprops.
move : (cdiff_pr cn1) (BS_diff \1c nB); set m := _ -c _ => nv mB.
set f1 := (fun i => omega0 ^o Vg X i).
have ha: ord_below_n f1 (\1c +c m).
   move => i; rewrite nv => lin; apply:(OS_pow OS_omega (proj1 ax1 _ lin)).
have hb: ordinalp (Vg X \0c) by apply:(proj1 ax1); apply/strict_pos_P1.
have hc:= (OS_pow OS_omega hb).
move: xv; rewrite /CNFrv /CNFrv0 -/n -nv.
rewrite (osum_expansionA BS1 mB ha) (osum_expansion1 (f := f1) hc) {2} /f1.
rewrite -/(CNFrv0 _ _); set f2:= (fun i : Set => Vg X (i +c \1c)).
have ax3: CNFr_ax0 f2 m.
  split.
    move => i im; apply: (proj1 ax1); rewrite - nv (csumC \1c).
    apply:csum_Mlteq; fprops.
  move => i iB sim.
  have eq: (succ i +c \1c) = succ (i +c \1c) by rewrite (csum_via_succ1 _ iB).
  rewrite /f2 eq; apply:(proj2 ax1); fprops.
  rewrite - nv (csumC \1c) - eq; apply:csum_Mlteq; fprops.
move:(OS_CNFr0 mB ax3); set a := CNFrv0 f2 m => oa.
case (equal_or_not (Vg X \0o) \0o)=> ez.
  rewrite ez opowx0 (ord_succ_pr oa) => xsa.
  by move:(ord_succ_lt oa); rewrite -xsa; move/lx => []; rewrite - xsa.
exists a,(Vg X \0c);split => //.
case: (equal_or_not m \0c) => mz.
  by left; rewrite /a mz /CNFrv0 osum_expansion0.
have cm1: \1c <=c m by apply: card_ge1; fprops.
move : (cdiff_pr cm1) (BS_diff \1c mB); set m' := _ -c _ => mv m'B.
set f1' := (fun i => omega0 ^o (f2 i)).
have oo1:ordinalp (f1' \0c).
  by apply: (OS_pow OS_omega);apply:(proj1 ax3); apply/strict_pos_P1.
have ha': ord_below_n f1' (\1c +c m').
  move => i il; apply: (OS_pow OS_omega); apply: (proj1 ax3); ue.
have sn0:succ \0c <c n by rewrite - nv succ_zero;apply:finite_sum4_lt; fprops.
have ez0: Vg X \0c <=o Vg X \1c.
  by move: (proj2 ax1 _ BS0 sn0); rewrite succ_zero.
have ez': \0o <o Vg X \1c.
  split; first by move: (ez0) => [h1 h2 _]; ord_tac1.
  move => b; case ez;rewrite - b in ez0; exact: (ord_le0 ez0).
move:(osum_expansionA BS1 m'B ha'); rewrite mv -/(CNFrv0 _ _) -/a.
rewrite (osum_expansion1 oo1); rewrite /f1' /f2 (csum0l CS1) => eq2.
have ax4: CNFr_ax0 (fun z : Set => Vg X ((z +c \1c) +c \1c)) m'.
  split.
    move => i im; apply: (proj1 ax3); rewrite - mv (csumC \1c).
    apply:csum_Mlteq; fprops.
  move => i iB sim.
  have eq: (succ i +c \1c) = succ (i +c \1c) by rewrite (csum_via_succ1 _ iB).
  rewrite /f2 eq; apply:(proj2 ax3); fprops.
  rewrite - mv (csumC \1c) - eq; apply:csum_Mlteq; fprops.
have sa:= (OS_CNFr0 m'B ax4).
have sb:= (opow_Momega_le ez0).
have la: limit_ordinal a.
 rewrite eq2;exact:(osum_limit sa (indecomp_limit2 ez')).
have le3: omega0 ^o Vg X \0c <=o a.
  rewrite eq2; apply: (ord_leT sb); apply: (osum_M0le sa (proj32 sb)).
right; split => //.
rewrite xv (osum_cardinal oa hc).
move: (ordinal_cardinal_le1 le3) => pc.
have pb: omega0 <=o omega0 ^o (Vg X \0c).
   rewrite - {1} (opowx1 OS_omega); apply: opow_Momega_le; fprops.
move: (ordinal_cardinal_le1 (ord_leT pb le3)).
rewrite (card_card CS_omega) => pd.
by apply: sum2_infinite => //; apply: (ge_infinite_infinite omega_infinitec).
Qed.

General Cantor Normal Form


Definition cantor_mon b (e c: fterm) i := (b ^o (e i)) *o (c i).
Definition CNFbv b e c n := osum_expansion (cantor_mon b e c) n.

Definition CNFq_ax b (e c: fterm) n :=
  [/\ \2o <=o b,
    ord_below_n e n,
    (forall i, i <c n -> c i <o b) &
    (forall i, inc i Bnat -> (succ i) <c n -> (e i) <o (e (succ i)))].

Definition CNFb_ax b e c n :=
  CNFq_ax b e c n /\ (forall i, i<c n -> \0o <o c i).

Lemma CNFq_ax_exten b e1 c1 e2 c2 n:
  same_below e1 e2 n -> same_below c1 c2 n ->
  CNFq_ax b e1 c1 n -> CNFq_ax b e2 c2 n.
Proof.
move => h1 h2 [a1 a2 a3 a4]; split => //.
+ by move => i lin; rewrite - (h1 _ lin);apply: a2.
+ by move => i lin; rewrite - (h2 _ lin);apply: a3.
+ move => i iB lin; rewrite - (h1 _ lin).
  by rewrite -(h1 _ (card_le_ltT (card_le_succ iB) lin)); apply:a4.
Qed.

Lemma CNFb_ax_exten b e1 c1 e2 c2 n:
  same_below e1 e2 n -> same_below c1 c2 n ->
  CNFb_ax b e1 c1 n -> CNFb_ax b e2 c2 n.
Proof.
move => h1 h2 [ax1 ax2]; split; first by apply:(CNFq_ax_exten h1 h2 ax1).
by move => i lin; rewrite - (h2 _ lin);apply: ax2.
Qed.

Lemma CNFq_exten b e1 c1 e2 c2 n:
  same_below e1 e2 n -> same_below c1 c2 n ->
  CNFq_ax b e1 c1 n -> inc n Bnat ->
  (CNFq_ax b e2 c2 n /\ CNFbv b e1 c1 n = CNFbv b e2 c2 n).
Proof.
move => h1 h2 ax nB; split; first by apply: (CNFq_ax_exten h1 h2 ax).
apply: (osum_expansion_exten nB) => i lin.
by rewrite /cantor_mon (h1 _ lin) (h2 _ lin).
Qed.

Lemma CNFb_exten b e1 c1 e2 c2 n:
  same_below e1 e2 n -> same_below c1 c2 n ->
  CNFb_ax b e1 c1 n -> inc n Bnat ->
  (CNFb_ax b e2 c2 n /\ CNFbv b e1 c1 n = CNFbv b e2 c2 n).
Proof.
move => h1 h2 [ax1 ax2] nB.
move: (CNFq_exten h1 h2 ax1 nB) => [ax3 ->]; split => //; split => //.
by move => i lin; rewrite - (h2 _ lin);apply: ax2.
Qed.

Lemma CNFq_p0 b e c n i: CNFq_ax b e c n -> i <c n ->
  ordinalp (cantor_mon b e c i).
Proof.
move => [pa pb pc pd] lin.
apply:OS_prod2; first by apply:(OS_pow (proj32 pa) (pb _ lin)).
exact:(proj31_1 (pc _ lin)).
Qed.

Lemma OS_CNFq b e c n : inc n Bnat -> CNFq_ax b e c n ->
  ordinalp (CNFbv b e c n).
Proof.
by move => nb h; apply:(OS_osum_expansion nb) => i /(CNFq_p0 h).
Qed.

Lemma OS_CNFb b e c n : inc n Bnat -> CNFb_ax b e c n ->
  ordinalp (CNFbv b e c n).
Proof. by move => nB [/(OS_CNFq nB) h _]. Qed.

Lemma CNFq_p1 b e c n: inc n Bnat ->
  CNFbv b e c (succ n) = cantor_mon b e c n +o (CNFbv b e c n).
Proof.
by move => nB; rewrite /CNFbv (osum_expansion_succ _ nB).
Qed.

Lemma CNFq_p2 b e c: CNFbv b e c \0c = \0o.
Proof. apply: osum_expansion0. Qed.

Lemma CNFq_p3 b e c n : CNFq_ax b e c n -> \0o <c n ->
   CNFbv b e c \1c = cantor_mon b e c \0c.
Proof. move => h np;apply: osum_expansion1; apply: (CNFq_p0 h np). Qed.

Lemma CNFq_p4 b e c n i: CNFb_ax b e c n -> i <c n ->
  \0o <o cantor_mon b e c i.
Proof.
move => [[pa pb pc pd] pe] lin.
apply: oprod2_pos; last by exact(pe _ lin).
exact:(opow_pos (ord_lt_leT (ord_lt_02) pa) (pb _ lin)).
Qed.

Lemma CNFq_r_ax b e c n m: CNFq_ax b e c n -> m <=c n -> CNFq_ax b e c m.
Proof.
move => [p1 p2 p3 p4] mn; split.
+ done.
+ move => i im; apply: p2; co_tac.
+ move => i im; apply: p3; co_tac.
+ move => i iB im; apply: p4 => //; co_tac.
Qed.

Lemma CNFb_r_ax b e c n m: CNFb_ax b e c n -> m <=c n -> CNFb_ax b e c m.
Proof.
move => [p1 p2] mn; split; first by exact: (CNFq_r_ax p1 mn).
by move => i im; apply: p2; co_tac.
Qed.

Lemma CNFq_p5 b e c n: inc n Bnat -> CNFq_ax b e c (succ n) ->
  CNFq_ax b e c n.
Proof. by move => nB ax; apply:(CNFq_r_ax ax (card_le_succ nB)). Qed.

Lemma CNFb_p5 b e c n: inc n Bnat -> CNFb_ax b e c (succ n) ->
  CNFb_ax b e c n.
Proof. by move => nB ax; apply:(CNFb_r_ax ax (card_le_succ nB)). Qed.

Lemma CNF_exponents_M b e c n: inc n Bnat -> CNFq_ax b e c n ->
  forall i j, i <=c j -> j <c n -> e i <=o e j.
Proof.
move => nB [_ pb _ pc] i j lij ljn.
have lin:=(card_le_ltT lij ljn).
have iB := (BS_lt_int lin nB).
pose r j := e i <=o e j.
have ri:=(ord_leR (pb _ lin)).
case: (equal_or_not n \0c) => nz.
  by move: lin; rewrite nz; move /card_lt0.
move: (cpred_pr nB nz) => [mB mv].
have jcn: j <=c cpred n by apply /(card_lt_succ_leP mB); rewrite -mv.
move: (cardinal_c_induction3 (r := r) iB mB ri)=> h.
apply: (h _ j lij jcn) => k ik kn; rewrite /r => le1.
have kB:= (BS_lt_int kn mB).
have skn : succ k <c n.
  by rewrite mv; apply/(card_lt_succ_leP mB) /(card_le_succ_ltP _ kB).
move:(pc k kB skn) => [lt1 _]; ord_tac.
Qed.

Lemma CNF_exponents_sM b e c n: inc n Bnat -> CNFq_ax b e c n ->
  forall i j, i <c j -> j <c n -> e i <o e j.
Proof.
move => nB ax i j lij ljn.
have iB := (BS_lt_int (card_lt_ltT lij ljn) nB).
move /(card_le_succ_ltP j iB) :lij => leij.
move:(CNF_exponents_M nB ax leij ljn) => sa.
move: ax => [_ _ _ ax]; move: (ax i iB (card_le_ltT leij ljn)) => h; ord_tac.
Qed.

Lemma CNF_exponents_I b e c n: inc n Bnat -> CNFq_ax b e c n ->
  forall i j, i <c n -> j <c n -> e i = e j -> i = j.
Proof.
move => nB /(CNF_exponents_sM nB) => m i j lin ljn eq.
case: (card_le_to_ell (proj31_1 lin) (proj31_1 ljn)) => cp.
+ exact.
+ by move: (proj2 (m i j cp ljn)); rewrite eq.
+ by move: (proj2 (m j i cp lin)); rewrite eq.
Qed.

Lemma CNFq_p6 b e c n: inc n Bnat -> CNFq_ax b e c (succ n) ->
  forall i, i <c n -> e i <o e n.
Proof.
move => nB ax i lin.
exact:(CNF_exponents_sM (BS_succ nB) ax lin (card_lt_succ nB)).
Qed.

Lemma CNFq_p7 b e c n : CNFq_ax b e c n -> \1c <c n ->
   CNFbv b e c \2c = cantor_mon b e c \1c +o cantor_mon b e c \0c.
Proof.
move:card_le_01 => l01 ax n1.
rewrite - succ_one (CNFq_p1 _ _ _ BS1) (CNFq_p3 (n:=n) ax) //; co_tac.
Qed.

Lemma CNFb_p8 b e c n : CNFb_ax b e c (succ n) -> inc n Bnat ->
  ordinalp (e n).
Proof. move => [[_ h _ _] _] nB; exact: (h _ (card_lt_succ nB)). Qed.

Definition cnf_s (f: fterm) k := (fun z => f (z +c k)).
Definition cnf_m (f1 f2:fterm) k := (fun z => Yo (z <c k) (f1 z) (f2 (z -c k))).
Definition cnf_change_n (f:fterm) n x := (fun z => Yo (z=n) x (f z)).

Lemma CNFq_s_ax b e c n k m:
  CNFq_ax b e c m -> (n +c k) <=c m -> inc k Bnat -> inc n Bnat ->
  CNFq_ax b (cnf_s e k) (cnf_s c k) n.
Proof.
move => [p1 p2 p3 p4] mn kB nB.
have aux: forall i, i <c n -> i +c k <c m.
  move => i lin; move:(csum_Mlteq kB nB lin) => h; co_tac.
split.
+ done.
+ by move => i /aux /p2.
+ by move => i /aux /p3.
+ move => i iB /aux; rewrite /cnf_s (csum_via_succ1 _ iB); apply: p4; fprops.
Qed.

Lemma CNFb_s_ax b e c n k m:
  CNFb_ax b e c m -> (n +c k) <=c m -> inc k Bnat -> inc n Bnat ->
  CNFb_ax b (cnf_s e k) (cnf_s c k) n.
Proof.
move => [p1 p2] mn kB nB; split; first by apply: (CNFq_s_ax p1 mn kB nB).
move => i lin; apply: p2; move:(csum_Mlteq kB nB lin) => h; co_tac.
Qed.

Lemma CNFq_m_ax b e1 c1 e2 c2 k m:
   inc k Bnat -> inc m Bnat ->
   CNFq_ax b e1 c1 k -> CNFq_ax b e2 c2 m ->
   (m = \0c \/ e1 (cpred k) <o e2 \0o) ->
   (CNFq_ax b (cnf_m e1 e2 k) (cnf_m c1 c2 k) (k +c m)).
Proof.
move => kB mB [p1 p2 p3 p4] [q1 q2 q3 q4] hs.
have aux: forall i, i <c k +c m -> i <c k \/ (~ (i <c k) /\ (i -c k) <c m).
  move => i lik.
  move:(BS_lt_int lik (BS_sum kB mB))=> iB.
  case: (card_le_to_el (CS_Bnat kB) (CS_Bnat iB)); last by left.
  move => ki; move: (cdiff_pr ki) => s1.
  right; split; first by move=> h; co_tac.
  apply: (csum_lt_simplifiable kB (BS_diff k iB) mB); ue.
rewrite/cnf_m; split.
+ done.
+ move => i /aux []; first by move => ik;by Ytac0; apply: p2.
  by move => [nik likm]; Ytac0; apply: q2.
+ move => i /aux []; first by move => ik;by Ytac0; apply: p3.
  by move => [nik likm]; Ytac0; apply: q3.
+ move => i iB lis; case:(aux _ lis).
    move => lt1; move: (card_le_ltT (card_le_succ iB) lt1) => li1.
    by Ytac0; Ytac0; apply:p4.
  move => [pa pb]; Ytac0.
  case: hs => hs.
    by move: pb; rewrite hs => /card_lt0.
  have ci:= (CS_Bnat iB).
  have ck:= (CS_Bnat kB).
  case: (card_le_to_ell ck (CS_succ i)) => //.
    move:(card_lt_succ iB) => lt1 sa; rewrite sa cdiff_n_n; Ytac0.
    have -> //: i = cpred k by rewrite sa cpred_pr1.
  move => /(card_lt_succ_leP iB) ki.
  case: (aux _ (card_le_ltT (card_le_succ iB) lis));first by move => ik; co_tac.
  move => [pc pd]; Ytac0.
  have sa: succ i -c k = succ (i-c k).
    move: (cdiff_pr4 kB iB BS0 BS1 ki card_le_01).
    rewrite (card_succ_pr4 ci) (csum0r ck) (cdiff_n_0 BS1) card_succ_pr4 //.
    co_tac.
  rewrite sa; apply: (q4 _ (BS_diff k iB)); ue.
Qed.

Lemma CNFb_m_ax b e1 c1 e2 c2 k m:
   inc k Bnat -> inc m Bnat ->
   CNFb_ax b e1 c1 k -> CNFb_ax b e2 c2 m ->
   (m = \0c \/ e1 (cpred k) <o e2 \0o) ->
   (CNFb_ax b (cnf_m e1 e2 k) (cnf_m c1 c2 k) (k +c m)).
Proof.
move => kB mB [p1 p2] [p3 p4] h1.
split; first by apply:CNFq_m_ax.
have aux: forall i, i <c k +c m -> i <c k \/ (~ (i <c k) /\ (i -c k) <c m).
  move => i lik.
  move:(BS_lt_int lik (BS_sum kB mB))=> iB.
  case: (Bnat_to_el kB iB); last by left.
  move => ki; move: (cdiff_pr ki) => s1.
  right; split; first by move=> h; co_tac.
  apply: (csum_lt_simplifiable kB (BS_diff k iB) mB); ue.
move => i /aux []; first by move => ik;by rewrite /cnf_m; Ytac0; apply: p2.
  by move => [nik likm]; rewrite /cnf_m; Ytac0; apply: p4.
Qed.

Lemma CNF_change_n_ax b e c n c0 k:
   \0o <o c0 -> c0 <o b ->
   CNFb_ax b e c n -> CNFb_ax b e (cnf_change_n c k c0) n.
Proof.
move => c1 c2 [[p1 p2 p3 p4] p5]; rewrite/cnf_change_n.
split; [split => // |]; move => i lin; Ytac cc => //; fprops.
Qed.

Definition CNFb_axo := CNFb_ax omega0.
Definition CNFbvo := CNFbv omega0.

Lemma CNFb_change_nv e c n m (c':= (cnf_change_n c n (m +o (c n)))):
  inc n Bnat -> CNFb_axo e c (succ n) -> m <o omega0 ->
  (CNFb_axo e c' (succ n) /\
    CNFbvo e c' (succ n) = omega0 ^o (e n) *o m +o CNFbvo e c (succ n)).
Proof.
move => nB ax mo.
have nn:= card_lt_succ nB.
have om: ordinalp m by ord_tac.
move: (ax) => [ [_ a0 a1 _] a2].
move: (a2 _ nn) => [[_ ocn _] nnz].
have pa:= (osum2_lt_omega mo (a1 _ nn)).
have pb: \0o <o m +o c n.
  apply: ord_ne0_pos; first by ord_tac.
  by move => h; move:(osum2_zero om ocn h) => [_ ]; apply: nesym.
move: (CNF_change_n_ax n pb pa ax); rewrite -/c' => ax2; split; first by exact.
have pc:= (OS_pow OS_omega (a0 _ nn)).
have pd:= CNFq_p0 (proj1 ax) nn.
have pe:=(OS_CNFq nB (CNFq_p5 nB (proj1 ax))).
rewrite /CNFbvo.
rewrite ! (CNFq_p1 _ _ _ nB) (osumA (OS_prod2 pc om) pd pe); apply: f_equal2.
  rewrite /cantor_mon /c' /cnf_change_n; Ytac0.
  by rewrite (osum_prodD om ocn pc).
apply: (osum_expansion_exten nB) => i [_ lin].
by rewrite /cantor_mon /c' /cnf_change_n; Ytac0.
Qed.

Lemma CNFq_A b e c n m:
  inc n Bnat -> inc m Bnat ->
   CNFq_ax b e c (n +c m) ->
   [/\ CNFq_ax b e c n, CNFq_ax b (cnf_s e n) (cnf_s c n) m &
    CNFbv b e c (n +c m) = CNFbv b (cnf_s e n) (cnf_s c n) m +o CNFbv b e c n].
Proof.
move => nB mB ax.
have pa: ord_below_n (cantor_mon b e c) (n +c m).
  by move => i; apply:CNFq_p0.
rewrite /CNFbv (osum_expansionA nB mB pa).
have lt1: n <=c n +c m by apply:csum_M0le; fprops.
have hb: CNFq_ax b e c n by apply:(CNFq_r_ax ax lt1).
have hc //: CNFq_ax b (cnf_s e n) (cnf_s c n) m.
have hh:m +c n <=c n +c m by rewrite csumC;apply: card_leR;co_tac.
exact:(CNFq_s_ax ax hh nB mB).
Qed.

Lemma CNFb_A e c n m:
  inc n Bnat -> inc m Bnat ->
   CNFb_axo e c (n +c m) ->
   [/\ CNFb_axo e c n, CNFb_axo (cnf_s e n) (cnf_s c n) m &
    CNFbvo e c (n +c m) = CNFbvo (cnf_s e n) (cnf_s c n) m +o CNFbvo e c n].
Proof.
move => nB mB ax.
rewrite /CNFb_axo /CNFbvo.
have pa: ord_below_n (cantor_mon omega0 e c) (n +c m).
  by move:ax => [ax _] i; apply:CNFq_p0.
rewrite /CNFbv (osum_expansionA nB mB pa).
have lt1: n <=c n +c m by apply:csum_M0le; fprops.
have hb: CNFb_ax omega0 e c n by apply:(CNFb_r_ax ax lt1).
rewrite csumC in pa.
have hc //: CNFb_ax omega0 (cnf_s e n) (cnf_s c n) m.
have hh:m +c n <=c n +c m by rewrite csumC;apply: card_leR;co_tac.
exact:(CNFb_s_ax ax hh nB mB).
Qed.

Lemma CNFq_Al b e c n (e1 := fun z => e (succ z)) (c1 := fun z => c (succ z)):
  inc n Bnat ->
   CNFq_ax b e c (succ n) ->
   [/\ ordinalp(cantor_mon b e c \0c), CNFq_ax b e1 c1 n &
    CNFbv b e c (succ n) = CNFbv b e1 c1 n +o (cantor_mon b e c \0c)].
Proof.
move => nB ax.
have h1: forall i, i<c n -> (cnf_s e \1c) i = e1 i.
  move => i lin; rewrite /cnf_s /e1 card_succ_pr4 //; co_tac.
have h2: forall i, i<c n -> (cnf_s c \1c) i = c1 i.
  by move => i lin; rewrite /cnf_s /c1 card_succ_pr4 //; co_tac.
have eq1: succ n = \1c +c n by rewrite csumC; exact:(Bsucc_rw nB).
rewrite eq1 in ax; move: (CNFq_A BS1 nB ax) => [sa sb sc].
have lt1: \0c <c (\1c +c n) by rewrite - eq1; apply: succ_positive.
rewrite eq1 sc (CNFq_p3 ax lt1).
move:(CNFq_exten h1 h2 sb nB) => [ax1 ->]; split => //.
by apply:(CNFq_p0 ax lt1).
Qed.

Lemma CNFb_Al e c n (e1 := fun z => e (succ z)) (c1 := fun z => c (succ z)):
  inc n Bnat ->
   CNFb_axo e c (succ n) ->
   [/\ ordinalp(cantor_mon omega0 e c \0o), CNFb_axo e1 c1 n &
    CNFbvo e c (succ n) = CNFbvo e1 c1 n +o (cantor_mon omega0 e c \0o)].
Proof.
move => nB [ax1 ax2]; move:(CNFq_Al nB ax1) => [sa sb sc]; split => //.
split => // i lin; apply: ax2.
by apply/(card_succ_succ_ltP (BS_lt_int lin nB) nB).
Qed.

Lemma CNFq_pg0 b e c n: CNFq_ax b e c n -> \0o <o b.
Proof. move => [pb _ _ _]; move: ord_lt_02 => h; ord_tac. Qed.

Lemma CNFq_pg1 b e c n: inc n Bnat -> CNFq_ax b e c (succ n) ->
  CNFbv b e c (succ n) <o (b ^o (succ_o (e n))).
Proof.
move: n;apply: cardinal_c_induction.
   move => h; rewrite succ_zero (CNFq_p3 h (succ_positive \0c)).
   move: (h) => [bo ax1 ax2 _ ].
   have szp:=(succ_positive \0c).
   move: (CNFq_pg0 h) (ax1 _ szp) (ax2 _ szp) => bp eo cb.
   rewrite /cantor_mon (opow_succ (proj32_1 bp) eo).
   exact:(oprod_Meqlt cb (opow_pos bp eo)).
move=> n nB Hrec ax1.
move: (Hrec (CNFq_p5 (BS_succ nB) ax1)) => sa.
move: (ax1) => [b2 _ ax3 ax2].
have snn:= (card_lt_succ (BS_succ nB)).
move: (ax2 n nB snn) (CNFq_p0 ax1 snn) => /ord_succ_ltP lt1 o1.
move:(ord_lt_leT sa (opow_Meqle (CNFq_pg0 ax1) lt1)) => lt2.
have ha: ordinalp (b ^o e (succ n)) by ord_tac.
move: (ax3 _ snn) => cm1.
have hb: ordinalp (c (succ n)) by ord_tac.
have lt3: b ^o e (succ n) *o succ_o (c (succ n)) <=o b ^o succ_o (e (succ n)).
  rewrite opow_succ; try ord_tac; apply: oprod_Meqle; last by ord_tac.
  by move /ord_succ_ltP: cm1.
move: (osum_Meqlt lt2 o1).
rewrite (CNFq_p1 _ _ _ (BS_succ nB)) {2}/cantor_mon - (oprod2_succ ha hb) => h1.
ord_tac.
Qed.

Lemma CNFq_pg2 b e c n a: inc n Bnat -> CNFq_ax b e c (succ n) ->
  (e n) <o a -> CNFbv b e c (succ n) <o (b ^o a).
Proof.
move => pa pb pc; move: (CNFq_pg1 pa pb) => h.
move/ord_succ_ltP: pc => pc.
exact: (ord_lt_leT h (opow_Meqle (CNFq_pg0 pb) pc)).
Qed.

Lemma CNFq_pg3 b e c n a: inc n Bnat -> CNFq_ax b e c n -> ordinalp a ->
  (forall i, i <c n -> e i <o a) ->
  CNFbv b e c n <o (b ^o a).
Proof.
move => nB ax oa h; move: (CNFq_pg0 ax) => bp.
case: (equal_or_not n \0c) => nz.
  rewrite nz CNFq_p2 //; apply: opow_pos; fprops.
move: (cpred_pr nB nz) => [qa qb].
rewrite qb in h ax.
have sa: (e (cpred n)) <o a by apply: h; apply: (card_lt_succ qa).
rewrite qb; exact:(CNFq_pg2 qa ax).
Qed.

Lemma CNFq_pg b e c n: inc n Bnat -> CNFq_ax b e c (succ n) ->
  CNFbv b e c n <o (b ^o (e n)).
move => nB ax.
move: (ax) => [_ ax2 _ _].
exact:(CNFq_pg3 nB (CNFq_p5 nB ax) (ax2 _ (card_lt_succ nB)) (CNFq_p6 nB ax)).
Qed.

Lemma CNFq_pg4 b e c n: inc n Bnat -> CNFb_ax b e c (succ n) ->
  (b ^o (e n)) <=o CNFbv b e c (succ n).
Proof.
move => nB [ax ax2]; move: (ax) => [b2 ax3 _ _].
have nn:= (card_lt_succ nB).
have pa:= (oprod_Mle1 (OS_pow (proj32 b2) (ax3 _ nn)) (ax2 _ nn)).
rewrite (CNFq_p1 _ _ _ nB).
move: (osum_Mle0 (proj32 pa) (OS_CNFq nB (CNFq_p5 nB ax))) => pb.
ord_tac.
Qed.

Lemma CNFq_pg5 b e c n: inc n Bnat -> CNFb_ax b e c (succ n) ->
  \0o <o CNFbv b e c (succ n).
Proof.
move => nB ax.
move: (opow_pos (CNFq_pg0 (proj1 ax)) (CNFb_p8 ax nB)) => cp.
exact:(ord_lt_leT cp (CNFq_pg4 nB ax)).
Qed.

Lemma CNFb_unique b e1 c1 n1 e2 c2 n2:
  inc n1 Bnat -> inc n2 Bnat -> CNFb_ax b e1 c1 n1 -> CNFb_ax b e2 c2 n2 ->
  CNFbv b e1 c1 n1 = CNFbv b e2 c2 n2 ->
  (n1 = n2 /\ forall i, i <c n1 -> e1 i = e2 i /\ c1 i = c2 i).
Proof.
move => n1B n2B; move: n1 n1B n2 n2B; apply: cardinal_c_induction.
  move=> n2 n2B ax1 ax2.
  case: (equal_or_not n2 \0c) => n2z.
    by rewrite n2z => _; split => // i /card_lt0.
  move: (cpred_pr n2B n2z) => [mb mv] eq.
  rewrite mv in ax2 eq.
    by move: (proj2 (CNFq_pg5 mb ax2)); rewrite - eq CNFq_p2;case.
move =>n1 n1B Hrec n2' n2'B ax1s ax2s sv.
case: (equal_or_not n2' \0c) => n2z.
  by move: (proj2 (CNFq_pg5 n1B ax1s)); rewrite sv n2z CNFq_p2; case.
move: (cpred_pr n2'B n2z) => []; set n2 := (cpred n2'); move => n2B n2v.
rewrite n2v in ax2s sv.
move: (card_lt_succ n1B) (card_lt_succ n2B) => lt1 lt2.
move: (ax1s) (ax2s) => [[u1 u2 u3 u4] u5] [[v1 v2 v3 v4] v5].
move: (u2 n1 lt1) (v2 n2 lt2) (u3 n1 lt1) (v3 n2 lt2) => oa1 oa2 of1 of2.
move: (u5 n1 lt1) (v5 n2 lt2) => ob1 ob2.
move: (proj32_1 ob1) (proj32_1 ob2) => oc1 oc2.
move: (CNFb_p5 n1B ax1s)(CNFb_p5 n2B ax2s) => ax1 ax2.
move: (OS_CNFq n1B (proj1 ax1)) (OS_CNFq n2B (proj1 ax2)) => oe1 oe2.
set a1 := CNFbv b e1 c1 (succ n1).
set a2 := CNFbv b e2 c2 (succ n2).
move: (erefl a1); rewrite {2} /a1 (CNFq_p1 _ _ _ n1B) => ha1.
move: (erefl a2); rewrite {2} /a2 (CNFq_p1 _ _ _ n2B) => ha2.
move: (CNFq_pg n1B (proj1 ax1s)) (CNFq_pg n2B (proj1 ax2s)) => hb1 hb2.
have og1:=(OS_CNFq (BS_succ n1B) (proj1 ax1s)).
have ox1: (ord_ext_div_pr b a1 (e1 n1) (c1 n1) (CNFbv b e1 c1 n1)).
  split;[ exact | exact| exact | split; [exact: ha1 | exact | exact | exact]].
have ox2: (ord_ext_div_pr b a1 (e2 n2) (c2 n2) (CNFbv b e2 c2 n2)).
  rewrite /a1 sv -/a2.
  split;[ exact | exact| exact | split; [exact: ha2 | exact | exact | exact]].
move: (ord_ext_div_unique u1 og1 ox1 ox2) => [se1 sc1 sr1].
move: (Hrec _ n2B ax1 ax2 sr1) => [n12 etc]; split.
   by rewrite n2v - n12.
move => i /(card_lt_succ_leP n1B); case: (equal_or_not i n1) => in1.
   by rewrite in1 {4 6} n12 => _; split.
by move => nin1; move: (etc _ (conj nin1 in1)).
Qed.

Lemma CNF_singleton b c0 e0 (c:= fun _: Set => c0)(e:= fun _: Set => e0):
  ordinalp e0 -> c0 <o b -> \2c <=o b ->
  [/\ CNFq_ax b e c \1c, CNFbv b e c \1c = b ^o e0 *o c0 &
    (\0o <o c0 -> CNFb_ax b e c \1c)].
Proof.
move=> oe co b2.
have aux: CNFq_ax b e c \1c.
  rewrite /e/c;split => // i ib.
  move: (@succ_positive i) => ha.
  rewrite - succ_zero;move/(card_lt_succ_leP BS0) => hb; co_tac.
by rewrite (CNFq_p3 aux card_lt_01).
Qed.

Lemma CNF_exp_bnd b e c n e0:
  \2c <=o b -> ordinalp e0 -> inc n Bnat ->
  CNFb_ax b e c n -> CNFbv b e c n <o b ^o e0 ->
  (forall i, i <c n -> e i <o e0).
Proof.
move => le1 oe nB ax lt1 i id.
case: (equal_or_not n \0c) => nz.
  by move: id; rewrite nz => /card_lt0.
move: (cpred_pr nB nz) => [mB mv].
rewrite mv in ax id.
move/(card_lt_succ_leP mB): id => ipn.
move:(CNF_exponents_M (BS_succ mB) (proj1 ax) ipn (card_lt_succ mB)) => ha.
case (ord_le_to_el oe (proj31 ha)) => // hb.
move:(CNFq_pg4 mB ax); rewrite - mv => h1; move:(ord_le_ltT h1 lt1) => hc.
move: (opow_Meqle (ord_lt_leT ord_lt_02 le1) (ord_leT hb ha)) => hd; ord_tac.
Qed.

Lemma CNFb_exists a b:
  ordinalp a -> \2c <=o b ->
  exists e c n, [/\ CNFb_ax b e c n, inc n Bnat & a = CNFbv b e c n].
Proof.
move=> oa oeb.
pose p a := exists e c n, [/\ CNFb_ax b e c n, inc n Bnat & a = CNFbv b e c n].
apply: (least_ordinal2 (p := p)) oa => y oy p2.
case: (equal_or_not y \0o) => ynz.
  exists (@id Set), (@id Set), \0c; split; first split.
  + split => // i; try move /card_lt0 => //.
    by move => _ /card_lt0.
  + by move => i /card_lt0.
  + fprops.
  + by rewrite CNFq_p2.
move: OS2 => o2.
have cpy1: \0o <o y by ord_tac1.
move: (ord_ext_div_exists oeb cpy1)
  => [e1 [c1 [rm [oe1 oc1 or [eq1 lt1 lt2 lt3]]]]].
have rmy: rm <o y.
  have p5: ordinalp (b ^o e1) by apply: OS_pow => //; ord_tac.
  have p3: (b ^o e1) <=o ((b ^o e1) *o c1) by apply: oprod_Mle1.
  move: (osum_Mle0 (proj32 p3) or); rewrite - eq1 => p4.
  exact : (ord_lt_leT lt1 (ord_leT p3 p4)).
move: (p2 _ rmy) => [e [c [n [ax nB rv]]]].
have snB:= (BS_succ nB).
pose e' i := Yo (i = n) e1 (e i).
pose c' i := Yo (i = n) c1 (c i).
exists e', c', (succ n).
have ha: CNFbv b e' c' n = CNFbv b e c n.
   rewrite /CNFbv; apply: osum_expansion_exten => // i [ _ lin].
   by rewrite /e' /c' /cantor_mon; Ytac0; Ytac0.
have hb: cantor_mon b e' c' n = b ^o e1 *o c1.
  by rewrite /cantor_mon /e' /c'; Ytac0; Ytac0.
rewrite (CNFq_p1 _ _ _ nB) ha - rv hb - eq1.
suff: CNFb_ax b e' c' (succ n) by move => hc; split.
move: (CNF_exp_bnd oeb oe1 nB ax); rewrite - rv => hx.
move: ax => [[a1 a2 a3 a4] a5]; split; last first.
  rewrite /c';move => i /(card_lt_succ_leP nB); case (equal_or_not i n).
    by move => -> _; Ytac0.
  move => i1 i2; Ytac0; exact: (a5 _ (conj i2 i1)).
split; first done.
+ rewrite /e';move => i /(card_lt_succ_leP nB); case (equal_or_not i n).
    by move => -> _; Ytac0.
  move => i1 i2; Ytac0; exact: (a2 _ (conj i2 i1)).
+ rewrite /c';move => i /(card_lt_succ_leP nB); case (equal_or_not i n).
    by move => -> _; Ytac0.
  move => i1 i2; Ytac0; exact: (a3 _ (conj i2 i1)).
+ rewrite /e';move => i iB /(card_lt_succ_leP nB) sin.
  have isi:= (card_lt_leT (card_lt_succ iB) sin).
  move: (proj2 isi) => nin; Ytac0.
  case (equal_or_not (succ i) n) => ne1; Ytac0; first by exact: (hx lt1 _ isi).
  exact:(a4 i iB (conj sin ne1)).
Qed.

Definition CNFbB n e c :=
   J n (J (Lg Bnat (fun z => Yo (z <c n) (e z) \0o))
          (Lg Bnat (fun z => Yo (z <c n) (c z) \0o))).

Section CNF_baseb.
Variable (b: Set).
Hypothesis bg2: \2o <=o b.

Definition cnfb_ax X :=
  [/\ pairp X, inc (P X) Bnat, pairp (Q X) &
   [/\ fgraph (P (Q X)), fgraph (Q (Q X)), domain (P (Q X)) = Bnat,
      domain (Q (Q X)) = Bnat &
   [/\ (forall i, inc i Bnat -> (P X) <=c i -> Vg (P (Q X)) i = \0o),
       (forall i, inc i Bnat -> (P X) <=c i -> Vg (Q (Q X)) i = \0o) &
    CNFb_ax b (Vg (P (Q X))) (Vg (Q (Q X))) (P X)]]].

Definition cnfbv X := CNFbv b (Vg (P (Q X))) (Vg (Q (Q X))) (P X).

Definition cnfb_bound x:=
   Bnat \times ((gfunctions Bnat (succ_o x)) \times (gfunctions Bnat b)).

Definition the_cnf x :=
  select (fun X => cnfb_ax X /\ cnfbv X = x) (cnfb_bound x).

Definition the_cnf_degree x :=
  (Vg (P (Q (the_cnf x))) (cpred (P (the_cnf x)))).

Lemma props_of_b: [/\ ordinalp b, b <> \0o & \0o <o b].
Proof.
move: bg2 => [_ ob _].
move: (ord_lt_leT (ord_lt_02) bg2) => bp.
move: (bp) => [_ /nesym bne].
split => //.
Qed.

Lemma cnfb_unique X1 X2: cnfb_ax X1 -> cnfb_ax X2 ->
   cnfbv X1 = cnfbv X2 -> X1 = X2.
Proof.
move => [p1 p2 p3 [p4 p5 p6 p7 [p8 p9 p10]]].
move => [q1 q2 q3 [q4 q5 q6 q7 [q8 q9 q10]]] sv.
move:(CNFb_unique p2 q2 p10 q10 sv) =>[sa sb].
have ha: P (Q X1) = P (Q X2).
  apply: fgraph_exten; [exact | exact | by rewrite p6 q6 | move => i id /=].
  rewrite p6 in id.
  case (card_le_to_el (CS_Bnat p2) (CS_Bnat id)) => h.
    by rewrite (p8 _ id h) (q8 _ id) - ?sa.
  exact (proj1 (sb _ h)).
have hb: Q (Q X1) = Q (Q X2).
  apply: fgraph_exten; [exact | exact | by rewrite p7 q7 | move => i id /=].
  rewrite p7 in id.
  case (card_le_to_el (CS_Bnat p2) (CS_Bnat id)) => h.
    by rewrite (p9 _ id h) (q9 _ id) - ?sa.
  exact (proj2 (sb _ h)).
have hc: Q X1 = Q X2 by apply:pair_exten.
by apply:pair_exten.
Qed.

Lemma cnfb_bound_p X: cnfb_ax X -> inc X (cnfb_bound (cnfbv X)).
Proof.
move => [p1 p2 p3 [p4 p5 p6 p7 [p8 p9 p10]]].
move: (p10) => [[p11 p12 p13 p14] p15].
move: (props_of_b) => [ob bnz bp].
apply/setX_P; split => //; apply/setX_P; split =>//.
  move: (OS_CNFq p2 (proj1 p10)) => osx.
  apply/graphset_P2; split => // v /(range_gP p4) [i]; rewrite p6 => iB ->.
  apply/(ord_leP osx).
  case: (Bnat_to_el p2 iB) => h; first by rewrite (p8 i iB h); ord_tac1.
  have ot:= (p12 _ h).
  move:(ord_leT (oprod_M1le bp ot)(opow_Mspec2 ot bg2)).
  move => ha; apply: (ord_leT ha).
  case: (equal_or_not (P X) \0c) => nz.
    by move: h; rewrite nz => /card_lt0.
  move: (cpred_pr p2 nz) => [mB mv].
  rewrite mv in p10 h.
  move:(CNFq_pg4 mB p10); rewrite - mv => eq1.
  have aa: i <=c (cpred (P X)) by apply /(card_lt_succ_leP mB).
  have bb: (cpred (P X)) <c succ (cpred (P X)) by apply:(card_lt_succ mB).
  move: (CNF_exponents_M (BS_succ mB) (proj1 p10) aa bb) => /(opow_Meqle bp).
  move => hc; ord_tac.
apply/graphset_P2; split => // v /(range_gP p5) [i]; rewrite p7 => iB ->.
case: (card_le_to_el (CS_Bnat p2) (CS_Bnat iB)) => h.
  by rewrite (p9 i iB h); apply: ord_ne_has0.
by move: (p13 i h) => /(ord_ltP ob).
Qed.

Lemma CNFbB_prop n e c: CNFb_ax b e c n -> inc n Bnat ->
   cnfb_ax (CNFbB n e c) /\ cnfbv (CNFbB n e c) = CNFbv b e c n.
Proof.
move => ax nB.
move:(ax) => [[a1 a2 a3 a4] a5]; rewrite /CNFbB.
rewrite /cnfb_ax /cnfbv !(pr1_pair, pr2_pair).
set e1 := Lg _ _.
set c1 := Lg _ _.
have h1: same_below e (Vg e1) n.
  by move => i lin; rewrite /e1 (LVg_E _ (BS_lt_int lin nB)); Ytac0.
have h2: same_below c (Vg c1) n.
  by move => i lin; rewrite /c1 (LVg_E _ (BS_lt_int lin nB)); Ytac0.
move: (CNFb_exten h1 h2 ax nB) => [sa <-].
split => //; split; [fprops | exact | fprops |].
rewrite {1 2 3} /e1 {1 2 3} /c1; bw; split; fprops; split => //.
  move => i iB ni; bw; Ytac h; [ co_tac | done].
move => i iB ni; bw; Ytac h; [ co_tac | done].
Qed.

Lemma cnfb_exists x: ordinalp x ->
   exists2 X, cnfb_ax X & cnfbv X = x.
Proof.
move => ox.
move: (CNFb_exists ox bg2) => [e [c [n [ax nB ->]]]].
by move: (CNFbB_prop ax nB) => [sa sb];exists (CNFbB n e c).
Qed.

Lemma the_cnf_p0 x (X:= the_cnf x): ordinalp x -> cnfb_ax X /\ cnfbv X = x.
Proof.
move => ox.
suff: (cnfb_ax X /\ cnfbv X = x) /\ inc X (cnfb_bound x) by move => [].
apply: select_pr.
  move: (cnfb_exists ox) => [z za zb]; exists z => //.
  by rewrite - zb ; apply:cnfb_bound_p.
move => a b' _ [p1 p2] _ [p3 p4].
rewrite - p4 in p2;exact:(cnfb_unique p1 p3 p2).
Qed.

Lemma cnfb_ax_simp X: cnfb_ax X ->
  inc (P X) Bnat /\ CNFb_ax b (Vg (P (Q X))) (Vg (Q (Q X))) (P X).
Proof. by move => [ _ p2 _ [_ _ _ _ [_ _ p10]]]. Qed.

Lemma the_cnf_p1: P(the_cnf \0o) = \0c.
Proof.
move:(the_cnf_p0 OS0) => [/cnfb_ax_simp [p2 p10] sb].
ex_middle nz.
move: (cpred_pr p2 nz) => [mB mv].
rewrite mv in p10.
by move:(proj2 (CNFq_pg5 mB p10)); rewrite -mv -/(cnfbv _) sb.
Qed.

Lemma the_cnf_p2 x (m := (cpred (P (the_cnf x)))): \0o <o x ->
  inc m Bnat /\ P (the_cnf x) = succ m.
Proof.
move => [[ _ ox _] xnz].
move:(the_cnf_p0 ox) => [/cnfb_ax_simp [nB ax] sb].
case (equal_or_not (P (the_cnf x)) \0c) => nz.
  by move:xnz; rewrite - sb /cnfbv nz /CNFbvo CNFq_p2.
exact: (cpred_pr nB nz).
Qed.

Lemma the_cnf_p3 e c n: CNFb_ax b e c n -> inc n Bnat ->
  the_cnf (CNFbv b e c n) = (CNFbB n e c).
Proof.
move => ax nB.
have ox:=(OS_CNFq nB (proj1 ax)).
move:(CNFbB_prop ax nB) (the_cnf_p0 ox) => [sa sb] [sc sd].
rewrite - sd in sb.
symmetry; exact: (cnfb_unique sa sc sb).
Qed.

Lemma OS_the_cnf_degree x: ordinalp x -> ordinalp (the_cnf_degree x).
Proof.
move => /the_cnf_p0 [sa sb].
move: sa => [p1 p2 p3 [p4 p5 p6 p7 [p8 p9 p10]]].
rewrite /the_cnf_degree.
case (equal_or_not (P (the_cnf x)) \0c) => nz.
  rewrite nz /cpred setU_0 -/card_zero p8; fprops; rewrite nz; fprops.
move: (p10) => [[_ p12 _ _] _]; apply: p12.
move:(cpred_pr p2 nz) => [mB eq]; rewrite {2} eq; apply: (card_lt_succ mB).
Qed.

End CNF_baseb.

Definition CNFB_ax X :=
  [/\ pairp X, inc (P X) Bnat, pairp (Q X) &
   [/\ fgraph (P (Q X)), fgraph (Q (Q X)), domain (P (Q X)) = Bnat,
      domain (Q (Q X)) = Bnat &
   [/\ (forall i, inc i Bnat -> (P X) <=c i -> Vg (P (Q X)) i = \0o),
       (forall i, inc i Bnat -> (P X) <=c i -> Vg (Q (Q X)) i = \0o) &
    CNFb_axo (Vg (P (Q X))) (Vg (Q (Q X))) (P X)]]].

Definition CNFBv X := CNFbvo (Vg (P (Q X))) (Vg (Q (Q X))) (P X).

Definition CNFB_bound x:=
   Bnat \times ((gfunctions Bnat (succ_o x)) \times (gfunctions Bnat Bnat)).

Definition the_CNF x :=
  select (fun X => CNFB_ax X /\ CNFBv X = x) (CNFB_bound x).
Definition the_CNF_degree x :=
  (Vg (P (Q (the_CNF x))) (cpred (P (the_CNF x)))).

Lemma CNFB_unique X1 X2: CNFB_ax X1 -> CNFB_ax X2 ->
   CNFBv X1 = CNFBv X2 -> X1 = X2.
Proof. by apply:cnfb_unique. Qed.

Lemma CNFB_bound_p X: CNFB_ax X -> inc X (CNFB_bound (CNFBv X)).
Proof. apply:(cnfb_bound_p ord_le_2omega). Qed.

Lemma CNFB_exists x: ordinalp x ->
   exists2 X, CNFB_ax X & CNFBv X = x.
Proof. apply: (cnfb_exists ord_le_2omega).
Qed.

Lemma the_CNF_p0 x (X:= the_CNF x): ordinalp x -> CNFB_ax X /\ CNFBv X = x.
Proof. exact: (the_cnf_p0 ord_le_2omega). Qed.

Lemma CNFB_ax_simp X: CNFB_ax X ->
  inc (P X) Bnat /\ CNFb_axo (Vg (P (Q X))) (Vg (Q (Q X))) (P X).
Proof. by move => [ _ p2 _ [_ _ _ _ [_ _ p10]]]. Qed.

Lemma the_CNF_p1: P(the_CNF \0o) = \0c.
Proof. exact: (the_cnf_p1 ord_le_2omega). Qed.

Lemma the_CNF_p2 x (m := (cpred (P (the_CNF x)))): \0o <o x ->
  inc m Bnat /\ P (the_CNF x) = succ m.
Proof. exact: (the_cnf_p2 ord_le_2omega). Qed.

Lemma the_CNF_p3 e c n: CNFb_axo e c n -> inc n Bnat ->
  the_CNF (CNFbvo e c n) = (CNFbB n e c).
Proof. exact: (the_cnf_p3 ord_le_2omega). Qed.

Lemma OS_the_CNF_degree x: ordinalp x -> ordinalp (the_CNF_degree x).
Proof. exact: (OS_the_cnf_degree ord_le_2omega). Qed.

Lemma the_CNF_p4 x (n := the_CNF_degree x): \0o <o x ->
  omega0 ^o n <=o x /\ x <o omega0 ^o (succ_o n).
Proof.
move => xp; move: (the_CNF_p2 xp) => [].
set m := cpred _; move => mB mv.
move: xp => [[ _ ox _] xnz].
move:(the_CNF_p0 ox) => [/CNFB_ax_simp [nB ax] sb].
rewrite mv in ax; split.
  move:(CNFq_pg4 mB ax);rewrite -mv -/CNFbvo -/(CNFBv _) sb //.
move:(CNFq_pg1 mB (proj1 ax));rewrite -mv -/CNFbvo -/(CNFBv _) sb //.
Qed.

Lemma the_CNF_p5 e c n (x:= CNFbvo e c (succ n)):
  inc n Bnat -> CNFb_axo e c (succ n) ->
  \0o <o x /\ the_CNF_degree x = e n.
Proof.
move => nB ax.
move:(CNFq_pg5 nB ax) => xp.
split; first by exact.
move:(the_CNF_p2 xp).
rewrite /x /the_CNF_degree; rewrite(the_CNF_p3 ax (BS_succ nB)).
set m := (cpred (P (CNFbB (succ n) e c))); move => [mB].
have sm:= card_lt_succ mB.
rewrite /CNFbB; aw; move => /(succ_injective1 (CS_Bnat nB) (CS_Bnat mB)) ->.
by bw; Ytac0.
Qed.

Lemma the_CNF_degree_one: the_CNF_degree \1o = \0o.
Proof.
move:(proj1 (the_CNF_p4 ord_lt_01))(OS_the_CNF_degree OS1).
set n := the_CNF_degree \1o.
rewrite -(@opowx0 omega0) => sa sb.
case: (ord_zero_dichot sb) => // /opow_Momega_lt sc; ord_tac.
Qed.

Lemma the_CNF_degree_omega: the_CNF_degree omega0 = \1o.
Proof.
move:(the_CNF_p4 ord_lt_0omega)(OS_the_CNF_degree OS_omega).
set n := the_CNF_degree omega0.
rewrite -{2 3} (opowx1 OS_omega); move => [sa sb] sc.
case: (ord_le_to_el sc OS1); last by move /opow_Momega_lt => h; ord_tac.
move => pa; case (equal_or_not n \1o) => n1//.
by case: (proj2 sb); rewrite (ord_lt1 (conj pa n1)) succ_o_zero.
Qed.

Lemma the_CNF_split x (e:= the_CNF_degree x) (X:= (the_CNF x))
    (c:= Vg (Q (Q X)) (cpred (P X)))
    (r := CNFbvo (Vg (P (Q X))) (Vg (Q (Q X))) (cpred (P X))):
  \0o <o x -> [/\ \0o <o c, c <o omega0, r <o omega0 ^o e &
    x = omega0 ^o e *o c +o r].
Proof.
move => xp.
move:(the_CNF_p2 xp).
rewrite /e/c/r/X. set m := cpred _; move => [mB Pv].
move: (the_CNF_p0 (proj32_1 xp)) => [/CNFB_ax_simp [sa]].
rewrite /CNFBv Pv.
set E := (Vg (P (Q (the_CNF x)))); set C := (Vg (Q (Q (the_CNF x)))).
move => sb sc.
move: (sb) => [[a1 a2 a3 a4] a5].
split.
+ exact:(a5 _ (card_lt_succ mB)).
+ exact:(a3 _ (card_lt_succ mB)).
+ exact:(CNFq_pg mB (proj1 sb)).
+ by rewrite -{1} sc /CNFbvo (CNFq_p1 _ _ _ mB).
Qed.

Lemma the_CNF_p6 a e: ordinalp e -> \0o <o a -> a <o (omega0 ^o e) ->
  (the_CNF_degree a) <o e.
Proof.
move => oe ap lta.
have lt2:= (ord_le_ltT (proj1 (the_CNF_p4 ap)) lta).
have od:= (OS_the_CNF_degree (proj32_1 ap)).
by rewrite (opow_Meqltr ord_le_2omega od oe).
Qed.

Lemma ord_negl_p8 ep cp p en cn n:
  CNFb_axo ep cp (succ p) -> CNFb_axo en cn (succ n) ->
  inc p Bnat -> inc n Bnat -> ep p <o en n ->
  (CNFbvo ep cp (succ p)) <<o (CNFbvo en cn (succ n)).
Proof.
move => axp axn pB nB ln.
have snB:= BS_succ nB.
set x := CNFbvo en cn (succ n).
have aux: forall e c,
   c <o omega0 -> e <o (en n) -> ((omega0 ^o e) *o c) <<o x.
  move => e c cb ef; rewrite /x.
  have oe: ordinalp e by ord_tac.
  have oc: ordinalp c by ord_tac.
  have om:=(CNFq_p0 (proj1 axn) (card_lt_succ nB)).
  rewrite /CNFbvo (CNFq_p1 _ _ _ nB).
  apply: (ord_negl_sum (OS_prod2 (OS_pow OS_omega oe) oc) om).
     exact: (OS_CNFq nB (CNFq_p5 nB (proj1 axn))).
   apply: (ord_negl_p5 cb ef) (proj2 axn _ (card_lt_succ nB)).
move:p pB axp ln; apply: cardinal_c_induction.
  move => ax1 lt1; move:(ax1) => [[_ _ hc _] _].
  rewrite /CNFbvo succ_zero (CNFq_p3 (proj1 ax1) (succ_positive \0c)).
  exact: (aux _ _ (hc _ (succ_positive \0c)) lt1).
move => p pB Hrec ax1 l1.
have spB:= (BS_succ pB).
move: (CNFb_p5 spB ax1) => axr.
have spp:= (card_lt_succ spB).
move:(proj1 ax1) => [_ _ hc ha].
have h0:= (ord_lt_leT (ha p pB spp) (proj1 l1)).
have h1 :=(CNFq_p0 (proj1 ax1) spp).
have h6: cp (succ p) <o omega0 by apply: (hc _ spp).
have ox: ordinalp x by apply:OS_CNFb.
rewrite /CNFbvo (CNFq_p1 _ _ _ spB).
exact: (ord_negl_sum1 h1 (OS_CNFb spB axr) ox (aux _ _ h6 l1) (Hrec axr h0)).
Qed.

Lemma ord_negl_p7 x y: \0o <o x -> \0o <o y ->
  the_CNF_degree x <o the_CNF_degree y -> x <<o y.
Proof.
move => xp yp.
move:(the_CNF_p2 xp)(the_CNF_p2 yp).
move: (the_CNF_p0 (proj32_1 xp))(the_CNF_p0 (proj32_1 yp)).
rewrite /the_CNF_degree.
set p:= (cpred _); set q := (cpred _).
move => [/CNFB_ax_simp ax1 v1][/CNFB_ax_simp ax2 v2] [pB sp][nB sn] h.
rewrite sp in ax1; rewrite sn in ax2.
move: (ord_negl_p8 (proj2 ax1) (proj2 ax2) pB nB h).
by rewrite - sp - sn -/(CNFBv _) v1 -/(CNFBv _) v2.
Qed.

Lemma CNF_sum_pr1 eX cX eY cY n m p
  (eZ := cnf_m eY (cnf_s eX n) (succ p))
  (cZ := cnf_m cY (cnf_s cX n) (succ p)):
  inc n Bnat -> inc m Bnat -> inc p Bnat ->
  CNFb_axo eX cX (n +c m) ->
  CNFb_axo eY cY (succ p) ->
  eY p <o eX n -> (n = \0c \/ eX (cpred n) <o eY p) ->
  ( CNFb_axo eZ cZ (succ p +c m) /\
    CNFbvo eX cX (n +c m) +o CNFbvo eY cY (succ p) =
      CNFbvo eZ cZ (succ p +c m)).
Proof.
move=> nB mB pB ax ay lt1 plt2.
have spB:= (BS_succ pB).
move:(CNFb_A nB mB ax) => [ax4 ax5 ->].
have axz: CNFb_axo eZ cZ (succ p +c m).
  apply:(CNFb_m_ax spB mB ay ax5);right.
  by rewrite /cnf_s (csum0l (CS_Bnat nB)) (cpred_pr1 (CS_Bnat pB)).
split; first by exact.
have oY:=(OS_CNFb spB ay).
rewrite - (osumA (OS_CNFb mB ax5) (OS_CNFb nB ax4) oY).
move:(CNFb_A spB mB axz) => [au av ->].
apply f_equal2.
  apply:(osum_expansion_exten mB) => i lim.
  have ww: ~ (i +c succ p <c succ p).
    rewrite csumC=> h; move:(csum_M0le i (CS_succ p)) => h'; co_tac.
  rewrite /cantor_mon /eZ/cZ /cnf_m /cnf_s; Ytac0; Ytac0.
  by rewrite (cdiff_pr1 (BS_lt_int lim mB) spB).
have <-: CNFbvo eY cY (succ p) = CNFbvo eZ cZ (succ p).
  apply:(osum_expansion_exten spB) => i lim.
  by rewrite /eZ/cZ/cantor_mon /cnf_s /cnf_m; Ytac0; Ytac0.
case (equal_or_not n \0c) => nz; first by rewrite nz CNFq_p2 osum0l //.
move: ax4; move: (cpred_pr nB nz)=> [n'B ->] ax4.
by apply: (ord_negl_p8 ax4 ay n'B pB); case:plt2.
Qed.

Lemma CNF_sum_pr2 eX cX eY cY n m p
  (eZ := cnf_m eY (cnf_s eX (succ n)) (succ p))
  (cZ := cnf_m (cnf_change_n cY p ((cX n) +o (cY p)))
         (cnf_s cX (succ n)) (succ p))
  (Z:= CNFbB (succ p +c m) eZ cZ):
  inc n Bnat -> inc m Bnat -> inc p Bnat ->
  CNFb_axo eX cX (succ n +c m) ->
  CNFb_axo eY cY (succ p) ->
  eY p = eX n ->
  ( CNFb_axo eZ cZ (succ p +c m) /\
    CNFbvo eX cX ((succ n) +c m) +o CNFbvo eY cY (succ p) =
    CNFbvo eZ cZ (succ p +c m)).
Proof.
move=> nB mB pB ax ay eq1.
have nmB:= BS_sum nB mB.
have spB := BS_succ pB.
have snB:= (BS_succ nB).
have cdx1: succ n +c m = n +c succ m.
   by rewrite csum_via_succ // csum_via_succ1.
have nls: n <c succ n +c m.
  by rewrite cdx1;apply:(finite_sum4_lt nB);apply: succ_nz.
have pa: cX n <o omega0 by move:(ax) => [[_ _ ha _ ] _]; apply: ha.
move: (CNFb_change_nv pB ay pa)=> []; rewrite -/cY -/eY => ax4 v4.
move:(CNFb_A snB mB ax) => [ax5 ax6 ->].
move: (ax) => [[_ _ _ h2] _].
have axz: CNFb_axo eZ cZ (succ p +c m).
  apply:(CNFb_m_ax spB mB ax4 ax6).
  rewrite (cpred_pr1 (CS_Bnat pB)) /cnf_s (csum0l (CS_Bnat snB)).
  rewrite -/eY eq1; case (equal_or_not m \0c)=> mz; first by left.
  right; apply: (h2 _ nB); by apply:finite_sum4_lt.
split; first by exact.
have oY:= (OS_CNFb spB ay).
move: (CNFb_A spB mB axz) => [ax7 ax8 ->].
rewrite- (osumA (OS_CNFb mB ax6) (OS_CNFb snB ax5) oY); apply: f_equal2.
  apply: (osum_expansion_exten mB) => i im.
  have ww: ~ (i +c succ p <c succ p).
    rewrite csumC=> h; move:(csum_M0le i (CS_succ p)) => h'; co_tac.
  rewrite /cantor_mon /eZ/cZ /cnf_m /cnf_s; Ytac0; Ytac0.
  by rewrite (cdiff_pr1 (BS_lt_int im mB) spB).
have ->: CNFbvo eZ cZ (succ p) =
   omega0 ^o eY p *o cX n +o CNFbvo eY cY (succ p).
   rewrite - v4; apply: (osum_expansion_exten spB) => i im.
   by rewrite /cantor_mon /eZ /cZ /cnf_s /cnf_m; Ytac0; Ytac0.
have h1 :=(CNFq_p0 (proj1 ax5) (card_lt_succ nB)).
have ax9:= (CNFb_p5 nB ax5).
rewrite (CNFq_p1 _ _ _ nB) eq1 - (osumA h1 (OS_CNFb nB ax9) oY).
congr (ord_sum2).
case (equal_or_not n \0c) => nz.
  rewrite nz CNFq_p2 (osum0l oY); reflexivity.
move: ax9; move: (cpred_pr nB nz)=> [n'B eq]; rewrite eq => ax9.
apply: (ord_negl_p8 ax9 ay n'B pB).
by rewrite -/eY eq1; rewrite {2} eq; apply: h2 => //; rewrite - eq //.
Qed.

Lemma CNF_sum_pr3 eX cX eY cY n p
  (eZ := cnf_m eY (cnf_s eX (succ n)) (succ p))
  (cZ := (cnf_change_n cY p ((cX n) +o (cY p)))):
  inc n Bnat -> inc p Bnat ->
  CNFb_axo eX cX (succ n) ->
  CNFb_axo eY cY (succ p) ->
  eY p = eX n ->
  ( CNFb_axo eZ cZ (succ p) /\
    CNFbvo eX cX (succ n) +o CNFbvo eY cY (succ p) =
    CNFbvo eZ cZ (succ p)).
Proof.
move => nB pB ax ay h1.
have aux1: (succ p +c \0c) = succ p by aw; rewrite /succ; fprops.
have aux2: (succ n +c \0c) = succ n by aw; rewrite /succ; fprops.
rewrite - aux2 in ax.
move:(CNF_sum_pr2 nB BS0 pB ax ay h1); rewrite aux1 aux2 -/eZ.
set c2 := cnf_m _ _ _.
have pa: same_below eZ eZ (succ p) by [].
have pb: same_below c2 cZ (succ p).
  by move => i idn;rewrite /c2 /cZ /cnf_m/cnf_change_n; Ytac0.
move =>[sa ->]; exact: (CNFb_exten pa pb sa (BS_succ pB)).
Qed.

Lemma CNF_prod_pr1 eX cX p k
  (cZ := (cnf_change_n cX p ((cX p) *o k))):
  \0o <o k -> k <o omega0 ->
  inc p Bnat -> CNFb_axo eX cX (succ p) ->
  (CNFb_axo eX cZ (succ p) /\
    CNFbvo eX cX (succ p) *o k= CNFbvo eX cZ (succ p)).
Proof.
move => kz ko pB ax.
pose ck k := cnf_change_n cX p (cX p *o k).
rewrite /cZ -/(ck k).
have psp:= card_lt_succ pB.
have pa: \0o <o cX p by move: (ax) => [_]; apply.
have H: forall k, \0o <o k -> k <o omega0 -> CNFb_axo eX (ck k) (succ p).
  move => n na nb; apply:CNF_change_n_ax => //; first by apply: oprod2_pos.
  apply: oprod2_lt_omega => //.
  move: (ax) => [[_ _ a2 _] _]; exact:(a2 _ psp).
move: (H _ kz ko) => az; split; first by exact.
pose r k := CNFbvo eX cX (succ p) *o k = CNFbvo eX (ck k) (succ p).
have spB:= (BS_succ pB).
have oX:=(OS_CNFb spB ax).
have r1: r \1c.
  rewrite /r (oprod1r oX) ; apply: (osum_expansion_exten spB).
  move => i isp; rewrite /ck /cnf_change_n /cantor_mon; Ytac h=> //.
  rewrite h oprod1r //; ord_tac.
have kB: inc k Bnat by apply /olt_omegaP.
have k1: \1c <=c k.
  by apply: card_ge1; fprops => ekz; move: (proj2 kz); rewrite ekz.
apply: (cardinal_c_induction2 (r :=r) BS1 r1 _ kB k1).
move => n nB n1 rn.
have on:= Bnat_oset nB.
have ->: succ n = succ_o n by apply: succ_of_Bnat.
rewrite /r /ck (oprod2_succ oX on) rn.
have n0: \0o <o n.
  apply: ord_ne0_pos => // nz.
  move: card_lt_01 => h1; rewrite nz in n1; co_tac.
have no: n <o omega0 by apply/ olt_omegaP.
have ax2:=(H _ n0 no).
move: (CNF_sum_pr3 pB pB ax2 ax (erefl (eX p))) => [ax3 ->].
apply: (osum_expansion_exten spB) => i isb.
have->: ck n p +o cX p = cX p *o succ_o n.
   rewrite /ck /cnf_change_n; Ytac0; rewrite (oprod2_succ _ on) //; ord_tac.
by rewrite /cantor_mon /cnf_m; Ytac0.
Qed.

Lemma CNF_limit e c n:
  inc n Bnat -> CNFb_axo e c (succ n) -> \0o <o (e \0c) ->
  exists2 z, ordinalp z & CNFbvo e c (succ n) = omega0 *o z.
Proof.
move => nB ax h0.
have h1: forall k, inc k Bnat -> CNFb_axo e c (succ k) ->
  exists2 z, ordinalp z & cantor_mon omega0 e c k = omega0 *o z.
  move => k kB axk; rewrite /cantor_mon.
  have kp: \0c <=c k by fprops.
  move: (CNF_exponents_M (BS_succ kB) (proj1 axk) kp (card_lt_succ kB)) => ek.
  move: (ord_rev_pred (ord_lt_leT h0 ek)) => [op ->].
  have oo:= OS_omega.
  have ob:= OS_pow oo op.
  move: (proj2 axk _ (card_lt_succ kB)) => [[_ oc _] _].
  rewrite (opow_sum oo OS1 op) (opowx1 oo) - (oprodA oo ob oc).
  exists (omega0 ^o (e k -o \1o) *o c k); [ exact: (OS_prod2 ob oc) | done].
move: n nB ax; apply: cardinal_c_induction.
  move => ha; move: (h1 _ BS0 ha) =>[z z1 z2]; exists z => //.
  move: (proj1 ha); rewrite succ_zero /CNFbvo => hb.
  by rewrite (CNFq_p3 hb card_lt_01).
move => n nB Hrec ax.
rewrite /CNFbvo (CNFq_p1 _ _ _ (BS_succ nB)) -/CNFbvo.
move: (Hrec (CNFb_p5 (BS_succ nB) ax)) => [z1 oz1 ->].
move:(h1 _ (BS_succ nB) ax) => [z2 oz2 ->].
rewrite - (osum_prodD oz2 oz1 OS_omega); exists (z2 +o z1); fprops.
Qed.

Lemma CNF_limit0 e c n:
  inc n Bnat -> CNFb_axo e c (succ n) ->
  (exists2 y, ordinalp y & CNFbvo e c (succ n) = y +o omega0 ^o (e \0c)).
Proof.
move => nB ax.
move: (CNFb_Al nB ax) => [sa sb ->].
have osn:= (succ_positive n).
move: (proj2 ax _ (succ_positive n)) => cp.
move: (ax) => [[_ h1 h2 _] _].
have o1:= (OS_pow OS_omega (h1 _ osn)).
have o2:= (OS_diff OS1 (proj32_1 cp)).
have o3 := (OS_prod2 o1 o2).
move: (oprec_nat (proj2 ax _ (succ_positive n)) (h2 _ osn)) => eq1.
rewrite /cantor_mon eq1 (oprod2_succ o1 o2).
rewrite (osumA (OS_CNFb nB sb) o3 o1).
set y := (CNFbv _ _ _ _ +o _); exists y => //.
apply: (OS_sum2 (OS_CNFb nB sb) o3).
Qed.

Lemma CNF_limit1 e c n:
  inc n Bnat -> CNFb_axo e c (succ n) ->
  (e \0c) = \0o -> ~ (limit_ordinal (CNFbvo e c (succ n))).
Proof.
move => nb ax; move: (CNF_limit0 nb ax) => [z zv ->] ->.
rewrite opowx0 (ord_succ_pr zv) => lz.
move /(limit_ordinal_P1 (OS_succ zv)): lz => [ _ h].
by apply:(proj2 (osuccVidpred (OS_succ zv))); split => //; exists z.
Qed.

Lemma CNF_limit2 e c n:
  inc n Bnat -> CNFb_axo e c (succ n) ->
  \0o <o (e \0c) -> (limit_ordinal (CNFbvo e c (succ n))).
Proof.
move => nb ax h1.
move: (CNF_limit0 nb ax) => [z oz ->].
apply: osum_limit => //;apply: indecomp_limit2 => //.
Qed.

Lemma CNF_limit3 x: limit_ordinal x ->
  exists2 z, ordinalp z & x = omega0 *o z.
Proof.
move =>lx.
move: (the_CNF_p0 (proj31 lx)) => [ax xv].
move: (CNFB_ax_simp ax) => [sa sb].
move:(the_CNF_p2 (limit_positive lx)); set m := cpred _.
move => [mB pv]; rewrite pv in sb.
move:(sb)=> [[_ ha _ _] _].
move: (ha _ (succ_positive m)) (CNF_limit1 mB sb).
rewrite - pv -/(CNFBv _) xv => hb hc.
have sc: \0o <o Vg (P (Q (the_CNF x))) \0c.
  by apply: ord_ne0_pos => // nz; case: (hc nz).
by move: (CNF_limit mB sb sc);rewrite - pv -/(CNFBv _) xv.
Qed.

Lemma CNF_se_p e c e0 n (eY:= fun i => e0 +o e i):
   inc n Bnat -> CNFb_axo e c n -> ordinalp e0 ->
   (CNFb_axo eY c n /\
   CNFbvo eY c n = omega0 ^o e0 *o CNFbvo e c n).
Proof.
move => nB ax oe.
have aux: forall k, CNFb_axo e c k -> CNFb_axo eY c k.
 move => k [[pa pb pc pd] pe]; split; [split |] => //.
 + move => i /pb oei; rewrite /eY; fprops.
 + move => i iB /(pd _ iB) sa; rewrite /eY; apply: (osum_Meqlt sa oe).
   split; first by apply: aux.
rewrite /CNFbvo.
move:n nB ax;apply: cardinal_c_induction.
 by move => _; rewrite !CNFq_p2 oprod0r.
move => n nB Hr ax.
move: (CNFb_p5 nB ax) => ax1.
have oa:=(CNFq_p0 (proj1 ax) (card_lt_succ nB)).
have ob:= (OS_CNFb nB ax1).
have oc:= OS_pow OS_omega oe.
have od:= (CNFb_p8 ax nB).
move: ax => [[_ _ hb _] _].
move: (hb _ (card_lt_succ nB)) => [[og _ _] _].
rewrite (CNFq_p1 _ _ _ nB) (CNFq_p1 _ _ _ nB) (Hr ax1) (osum_prodD oa ob oc).
rewrite /eY /cantor_mon (opow_sum OS_omega oe od).
by rewrite (oprodA oc (OS_pow OS_omega od) og).
Qed.

Lemma CNF_prod_pr2 e c n:
  inc n Bnat -> CNFb_axo e c (succ n) ->
  CNFbvo e c (succ n) *o omega0 = omega0 ^o (e n) *o omega0.
Proof.
move=> nB ax; rewrite /CNFbvo.
have nn:= card_lt_succ nB.
move: (ax) => [[_ h1 h2 _] h3].
have h4:= (OS_pow OS_omega (h1 _ nn)).
have h5:= OS_prod2 h4 OS_omega.
have h3n:= (h3 _ nn).
apply: ord_leA; last first.
  have ox:= (OS_CNFb nB (CNFb_p5 nB ax)).
  apply: (oprod_Mleeq _ OS_omega); apply: (ord_leT (oprod_Mle1 h4 h3n)).
  rewrite (CNFq_p1 _ _ _ nB); apply: (osum_Mle0 (CNFq_p0 (proj1 ax) nn) ox).
set x := CNFbvo e c (succ n).
have pc' : \0o <o x by apply:(CNFq_pg5 nB ax).
have ox: ordinalp x by ord_tac.
move: (oprod_normal pc') => [pg pk].
rewrite (pk _ (omega_limit)); clear pk.
apply: ord_ub_sup => //.
  move=> t /funI_P [z zo ->]; apply: OS_prod2 => //.
  by apply: (ordinal_hi OS_omega zo).
move=> i /funI_P [z zo ->].
move: zo => /(ord_ltP OS_omega) zo.
have oz: ordinalp z by ord_tac.
case: (ord_zero_dichot oz) => zno.
  by rewrite zno (oprod0r); apply: ozero_least.
move: (oprod2_lt_omega (h2 _ nn) zo) => /ord_succ_ltP so.
move: (CNF_prod_pr1 zno zo nB ax) => [ax1 ->].
rewrite /CNFbvo (CNFq_p1 _ _ _ nB).
have lt1: CNFbvo e (cnf_change_n c n (c n *o z)) n <o omega0 ^o (e n).
  apply:(CNFq_pg3 nB (CNFq_p5 nB (proj1 ax1)) (h1 _ nn)).
    move => k kn; exact:(CNF_exponents_sM (BS_succ nB) (proj1 ax) kn nn).
rewrite {1} /cnf_change_n /cantor_mon; Ytac0.
have oy1:= (OS_prod2 (proj32_1 h3n) oz).
move: (osum_Meqlt lt1 (OS_prod2 h4 oy1)); rewrite - (oprod2_succ h4 oy1).
move => [le1 _]; apply: (ord_leT le1 (oprod_Meqle so h4)).
Qed.

Lemma CNF_prod_pr2bis x: \0o <o x->
  x *o omega0 = omega0 ^o (the_CNF_degree x) *o omega0.
Proof.
move => xp.
move: (the_CNF_p0 (proj32_1 xp)) => [ax0 xv].
move: (CNFB_ax_simp ax0) (the_CNF_p2 xp) => [pb ax] [nB pc].
by rewrite pc in ax; rewrite - (CNF_prod_pr2 nB ax) - {1} xv - pc.
Qed.

Lemma oprod_crit_aux n x (y := omega0 ^o (omega0 ^o n)):
  ordinalp n -> \1o <=o x -> x <o y -> x *o y = y.
Proof.
move => on x1 xy.
move: OS_omega OS1 ord_lt_1omega => oo o1 lt1o.
have oy1:= OS_pow OS_omega on.
have oy:= OS_pow OS_omega oy1.
have xp: \0o <o x by ord_tac1.
have yif: omega0 <=o y.
   rewrite /y - {1} (opowx1 OS_omega); apply: opow_Momega_le.
   by apply: ord_ge1 => //; apply: omega_pow_nz.
case: (ord_zero_dichot on) => nz.
  move: xy;rewrite /y nz opowx0 (opowx1 OS_omega) => aux2.
  rewrite oprod_int_omega //.
have aux1: omega0 *o (omega0 ^o (omega0 ^o n)) = omega0 ^o (omega0 ^o n).
  rewrite - {1} (opowx1 OS_omega) - opow_sum //;congr (_ ^o _).
  apply: ord_negl_p2 => //.
have ox: ordinalp x by ord_tac.
have od:=(OS_the_CNF_degree ox).
rewrite /y - aux1 (oprodA ox oo oy) (CNF_prod_pr2bis xp).
rewrite - (oprodA (OS_pow oo od) oo oy) aux1.
move: xy; rewrite - (opow_sum oo od oy1) => h2.
by rewrite (indecomp_prop1 (indecomp_prop4 on) (the_CNF_p6 oy1 xp h2)).
Qed.

Lemma CNF_prod_pr3 x y: \0o <o x-> limit_ordinal y ->
  x *o y = omega0 ^o (the_CNF_degree x) *o y.
Proof.
move=> xnz ly; move:(proj32_1 xnz) => ox.
move: (CNF_limit3 ly) => [z oz yv].
have ot := (OS_pow OS_omega (OS_the_CNF_degree ox)).
by rewrite yv (oprodA ox OS_omega oz) (CNF_prod_pr2bis xnz)
 (oprodA ot OS_omega oz).
Qed.

Lemma CNF_prod_pr4 eX cX n eY cY p
  (x:= CNFbvo eX cX (succ n)) (y:= CNFbvo eY cY (succ p)):
  inc n Bnat -> inc p Bnat ->
  CNFb_axo eX cX (succ n) -> CNFb_axo eY cY (succ p) ->
  \0o <o eY \0c -> x *o y = omega0 ^o (eX n) *o y.
Proof.
move=> nB pB ax ay pnz.
move: (CNF_limit2 pB ay pnz) => ly.
move: (the_CNF_p5 nB ax) => [xp dx].
by move:(CNF_prod_pr3 xp ly); rewrite -/y dx.
Qed.

Lemma CNF_prod_pr5 eX cX n eY cY p
      (eZ:= fun i => (eX n) +o eY i)
      (x:= CNFbvo eX cX (succ n)) (y:= CNFbvo eY cY (succ p)):
  inc n Bnat -> inc p Bnat ->
  CNFb_axo eX cX (succ n) -> CNFb_axo eY cY (succ p) ->
  \0o <o eY \0c ->
  (CNFb_axo eZ cY (succ p) /\ x *o y = CNFbvo eZ cY (succ p)).
Proof.
move=> nB pB ax ay pnz.
move: (CNF_se_p (BS_succ pB) ay (CNFb_p8 ax nB)) => [sa ->]; split => //.
by rewrite CNF_prod_pr4.
Qed.

Lemma CNF_prod_pr6 eX cX n eY cY p
  (x:= CNFbvo eX cX (succ n)) (y:= CNFbvo eY cY (succ p))
  (cZ := cnf_m (cnf_change_n cX n (cX n *o cY \0o))
      (fun z => cY (succ z)) (succ n))
  (eZ := cnf_m eX (fun z => (eX n) +o (eY (succ z))) (succ n)):
  inc n Bnat -> inc p Bnat ->
  CNFb_axo eX cX (succ n) -> CNFb_axo eY cY (succ p) ->
   eY \0c = \0o ->
  (CNFb_axo eZ cZ (succ (n +c p)) /\ x *o y = CNFbvo eZ cZ (succ (n +c p))).
Proof.
move => nB pB ax ay tcy.
rewrite /y.
have spp:= (succ_positive p).
move: (proj2 ay _ spp) => c0p.
have snB:= (BS_succ nB).
have oc0: ordinalp (cY \0c) by ord_tac.
have c0o: cY \0c <o omega0 by move:(ay)=> [[_ _ h _] _]; apply: (h _ spp).
have [om1 ay1 ->] := (CNFb_Al pB ay).
move: (OS_CNFb pB ay1) (OS_CNFb snB ax) => oy1 ox.
rewrite (osum_prodD oy1 om1 ox) /cantor_mon tcy opowx0 (oprod1l oc0).
move: (CNF_prod_pr1 c0p c0o nB ax) => [ax1 ->].
move: ax1; rewrite /cZ; set c1:= (cnf_change_n cX n (cX n *o cY \0c)) => ax1.
case (equal_or_not p \0o) => pnz.
  rewrite pnz (csum0r (CS_Bnat nB)) CNFq_p2 oprod0r (osum0l (OS_CNFb snB ax1)).
  apply:(CNFb_exten _ _ ax1 snB).
    by move => i lin; rewrite /eZ/cnf_m; Ytac0.
  by move => i lin; rewrite /cnf_m; Ytac0.
move: (cpred_pr pB pnz); set m := (cpred p); move => [mB mv].
rewrite mv in ay1; rewrite mv.
have cp1: (\0o <o eY (succ \0c)).
  have c1p: succ \0o <c succ p.
    apply/(card_succ_succ_ltP BS0 pB); rewrite mv; apply: succ_positive.
  have lt01:= succ_positive \0c.
  move:(CNF_exponents_sM (BS_succ pB) (proj1 ay) lt01 c1p) => h.
  apply: (ord_ne0_pos (proj32_1 h) (ord_gt_ne0 h)).
move:(CNF_prod_pr5 nB mB ax ay1 cp1) => [ax2 ->].
have sa: \0c +c succ m = succ m by rewrite csum0l; fprops.
have sb: eX n <o eX n +o eY (succ \0c).
  have h2:= CNFb_p8 ax nB.
  by move: (osum_Meqlt cp1 h2); rewrite (osum0r h2).
have sc: \0c = \0c \/ eX n +o eY (succ (cpred \0c)) <o eX n by left.
rewrite - sa in ax2 |- *.
move: (CNF_sum_pr1 BS0 (BS_succ mB) nB ax2 ax1 sb sc) => [ax3 ->].
rewrite sa - (csum_via_succ1 (succ m) nB).
have hh: forall k, (k -c (succ n)) +c \0c = (k -c (succ n)).
  move=> k; exact:(csum0r (CS_cardinal (k -s succ n))).
apply: (CNFb_exten _ _ ax3 (BS_sum (BS_succ nB) (BS_succ mB))).
  by move => i isn; rewrite/eZ /cnf_m /cnf_s hh.
by move => i isn; rewrite /cnf_m /cnf_s hh.
Qed.

Lemma CNF_succ_pow1 n c (x := (succ_o ((omega0 ^o n) *o c)))
   (X:= the_CNF x) (eX := (Vg (P (Q (the_CNF x)))))
   (cX := (Vg (Q (Q (the_CNF x))))):
  \0o <o n -> \0o <o c -> c <o omega0 ->
  [/\ CNFb_axo eX cX (P X), CNFbvo eX cX (P X) = x &
   [/\ P X = \2c, eX \0c = \0o, eX \1c = n, cX \0c = \1o & cX \1c = c]].
Proof.
move: OS0 => oz np cp lco.
move: ord_le_2omega BS2 BS1 => le2 bs2 bs1.
have oc: ordinalp c by ord_tac.
have on: ordinalp n by ord_tac.
have o1:= OS_pow OS_omega on.
have o2:= OS_prod2 o1 oc.
move: BS0 card_lt_02 card_lt_12 card_lt_01 => bs0 lt02 lt12 [_ n01].
set ex := fun z => Yo (z = \0c) \0o n.
set cx := fun z => Yo (z = \0c) \1o c.
have e0: ex \0c = \0o by rewrite /ex; Ytac0.
have e1: ex \1c = n by rewrite /ex; Ytac0.
have c0: cx \0c = \1o by rewrite /cx; Ytac0.
have c1: cx \1c = c by rewrite /cx; Ytac0.
have ax: CNFb_axo ex cx \2c.
  split; first split.
  + exact.
  + by move => i lin; rewrite /ex; Ytac h.
  + by move => i lin; rewrite /cx; Ytac h => //; apply: ord_lt_1omega.
  + move => i iB /card_lt2; rewrite /ex; move: (@succ_nz i) => ss.
    rewrite - succ_zero; case => // si.
    by move: (succ_injective1 (CS_Bnat iB) CS0 si) => iz; Ytac0; Ytac0.
  + by move => i lin; rewrite /cx; Ytac h => //; apply: ord_lt_01.
move: (CNFbB_prop ax BS2); set y := (CNFbB \2c ex cx); move => [ax2 yv].
have py2: P y = \2c by rewrite /y /CNFbB; aw.
move: (the_CNF_p0 (OS_succ o2)); rewrite -/x; move => [ax3 xv].
move: (CNFB_ax_simp ax2) => [_ ax4].
have eq1:CNFBv (the_CNF x) = CNFBv y.
  rewrite py2 in ax4.
  move: (CNFq_p7 (proj1 ax4) lt12).
  rewrite xv /CNFBv /y /CNFbB !(pr1_pair, pr2_pair) -/CNFbvo => ->.
  rewrite /cantor_mon; bw; repeat Ytac0; rewrite e0 c0 e1 c1.
  by rewrite opowx0 (oprod1r OS1) (ord_succ_pr o2).
move:(CNFB_unique ax3 ax2 eq1).
rewrite -/(CNFBv (the_CNF x)) xv /eX /cX -/X => ->; split.
+ exact.
+ exact.
+ by rewrite /y /CNFbB !(pr1_pair, pr2_pair); bw; repeat Ytac0; split.
Qed.

Lemma CNF_succ_pow n (x := (succ_o (omega0 ^o n)))
   (X:= the_CNF x) (eX := (Vg (P (Q (the_CNF x)))))
   (cX := (Vg (Q (Q (the_CNF x))))):
  \0o <o n ->
  [/\ CNFb_axo eX cX (P X), CNFbvo eX cX (P X) = x &
  [/\ P X = \2c, eX \0c = \0o, eX \1c = n, cX \0c = \1o & cX \1c = \1o]].
Proof.
move: ord_lt_01 ord_lt_1omega => hb hc ha.
move:(CNF_succ_pow1 ha hb hc).
by rewrite(oprod1r (OS_pow OS_omega (proj32_1 ha))).
Qed.

Lemma succ_pow_omega_irred p a b:
  ordinalp p -> ordinalp a -> ordinalp b ->
  succ_o (omega0 ^o p) = a *o b ->
  (a = \1o \/ b = \1o).
Proof.
move=>on oa ob sab.
case: (ord_zero_dichot on) => pz.
  by apply: oprod2_two => //; rewrite - sab pz opowx0 // succ_o_one.
move: (CNF_succ_pow pz).
set ep := Vg _ ; set cp := Vg _; set np:= (P (the_CNF _)).
move => [axp pv etc].
have snz: a *o b <> \0o by rewrite - sab;apply: succo_nz.
have anz: a <> \0o by move =>h; case: snz; rewrite h oprod0l.
have bnz: b <> \0o by move =>h; case: snz; rewrite h oprod0r.
have ap: \0o <o a by ord_tac1.
have bp: \0o <o b by ord_tac1.
move: (the_CNF_p0 oa) (the_CNF_p0 ob) => [sa sb][sc sd].
move: (CNFB_ax_simp sa) (CNFB_ax_simp sc) (the_CNF_p2 ap) (the_CNF_p2 bp).
move: sb sd; rewrite /CNFBv.
set ea := Vg _ ; set ca := Vg _; set na:= (P (the_CNF a)); set ma:=(cpred na).
set eb := Vg _ ; set cb := Vg _; set nb:= (P (the_CNF b)); set mb:=(cpred nb).
move => va vb [naB axa] [nbB axb] [maB mav] [mbB mbv].
rewrite mav in axa; rewrite mbv in axb.
move: (succ_positive ma)(succ_positive mb) => spa spb.
move: (axb)(axa) => [[_ h1b h2b _] _] [[_ h1a h2a _] _].
have oeb0:= (h1b _ spb).
have ocb0:= (proj31_1 (h2b _ spb)).
have oca0:= (proj31_1 (h2a _ spa)).
move: etc => [x0 x1 x2 x3 x4].
have npB: inc np Bnat by rewrite x0; fprops.
case (ord_zero_dichot oeb0) => ez.
  move: (CNF_prod_pr6 maB mbB axa axb ez).
  rewrite -mav -mbv va vb; move => [su sv].
  move: pv; rewrite sab sv => eq.
  have dB:= (BS_succ (BS_sum maB mbB)).
  move: (CNFb_unique npB dB axp su eq); rewrite x0; move => [ha hb].
  have nap: \0c <c na by rewrite mav; apply: succ_positive.
  have mab1: \1c = (ma +c mb).
    by apply: (succ_injective1 CS1 (CS_sum2 ma mb)); rewrite succ_one.
  move:(hb _ card_lt_02) (hb _ card_lt_12);rewrite x1 x2 x3 x4.
  rewrite /cnf_m /cnf_change_n; Ytac0; Ytac0.
  case (equal_or_not ma \0c) => maz.
    rewrite mav maz succ_zero; Ytac0; move => [ua ub].
    symmetry in ub; move: (oprod2_one oca0 ocb0 ub) => [ca0 _] _.
    left; rewrite - va mav maz succ_zero.
    rewrite /CNFbvo (CNFq_p3 (proj1 axa) spa).
    by rewrite /cantor_mon -ua ca0 opowx0 (oprod1r OS1).
  move: card_lt_12 => l12.
  case (equal_or_not mb \0c) => mbz _ [ _] .
    move:mab1; rewrite mbz (csum0r (CS_Bnat maB)) => ma1.
    rewrite mav - ma1 succ_one; Ytac0; Ytac0 => eq1.
    have hh: \1c <c succ ma by rewrite - ma1; apply: (card_lt_succ BS1).
    have oca1: ordinalp (ca \1c) by move: (h2a _ hh) => hh1; ord_tac.
    symmetry in eq1; move: (oprod2_one oca1 ocb0 eq1) => [_ cb0].
    right; rewrite - vb mbv mbz succ_zero.
    rewrite /CNFbvo (CNFq_p3 (proj1 axb) spb).
    by rewrite /cantor_mon ez cb0 opowx0 (oprod1r OS1).
  move: (card_ge1 (CS_Bnat maB) maz) (card_ge1 (CS_Bnat mbB) mbz).
  move => l1 l2; move: (csum_Mlele l1 l2); rewrite - mab1 card_two_pr.
  move => l12'; co_tac.
move: (CNF_prod_pr5 maB mbB axa axb ez).
rewrite -mav -mbv va vb; move => [su sv].
move: pv; rewrite sab sv => eq.
move: (CNFb_unique npB nbB axp su eq); rewrite x0; move => [ha hb].
move:(esym (proj1 (hb _ card_lt_02))); rewrite x1 => e1.
move:(osum2_zero (h1a _ (card_lt_succ maB)) oeb0 e1) => [_ h].
by move: (proj2 ez); rewrite h; case.
Qed.

Lemma opow_int_omega n:
  \2o <=o n -> n <o omega0 -> n ^o omega0 = omega0.
Proof.
move=> n2 no.
have oo:= OS_omega.
have on: ordinalp n by ord_tac.
have nz: \0o <o n by move: (ord_lt_leT ord_lt_02 n2).
apply:ord_leA.
  rewrite (proj2 (opow_normal n2) _ omega_limit).
  apply: ord_ub_sup => //.
    move=> v => /funI_P [z /(ordinal_hi oo) zy ->]; fprops.
  by move => x /funI_P [z /(ord_ltP oo) /(opow_2int1 no) [zo _] ->].
by move: (opow_Mspec2 oo n2); rewrite oprod_int_omega.
Qed.

Lemma CNF_pow_pr1 e c n k (x:= CNFbvo e c (succ n)):
  CNFb_axo e c (succ n) -> \0o <o e \0c ->
  inc k Bnat -> inc n Bnat ->
  x ^o (succ_o k) = (omega0 ^o ((e n) *o k)) *o x.
Proof.
move=> ax ep kB nB.
have ox:=(OS_CNFb (BS_succ nB) ax).
have olcx:= CNFb_p8 ax nB.
move: k kB; apply: cardinal_c_induction.
  by rewrite (oprod0r) opowx0 (oprod1l ox) succ_o_zero opowx1.
move=> k kB hrec.
move/BnatP: (kB) => p2.
have ok:= proj1 p2.
have osk:= OS_succ ok.
have odf:=(OS_prod2 olcx ok).
move: (OS_pow OS_omega odf)(OS_pow OS_omega olcx) => of1 ood.
rewrite (succ_of_finite p2) (opow_succ ox osk) hrec - (oprodA of1 ox ox).
rewrite (CNF_prod_pr4 nB nB ax ax ep) (oprodA of1 ood ox)(oprod2_succ olcx ok).
by rewrite - (opow_sum OS_omega odf olcx).
Qed.

Lemma CNF_pow_pr2 ex cx ey cy n m k:
  CNFb_axo ex cx (succ n) -> CNFb_axo ey cy m ->
  inc n Bnat -> inc m Bnat -> inc k Bnat -> k <> \0c -> \0o <o ex n ->
  (CNFbvo ex cx (succ n)) ^o k = (CNFbvo ey cy m) ->
  [/\ m <> \0c, ey (cpred m) = (ex n) *o k & cy (cpred m) = cx n].
Proof.
move => ax ay nB mB kB kp cnp.
move: (cpred_pr kB kp) => [pa pb].
have snB:= (BS_succ nB).
set q := cpred k in pa pb; rewrite pb.
clear kB kp pb; move: q pa m ey cy mB ay; clear k.
have ox:= OS_CNFb snB ax.
have lts:=(card_lt_succ nB).
have oo: ordinalp (ex \0o).
  move: (ax) =>[[_ h1 _ _] _]; exact: (h1 _ (succ_positive n)).
have op:= CNFb_p8 ax nB.
apply: cardinal_c_induction.
  move=> m ey cy mB ay.
  rewrite succ_zero (opowx1 ox) (oprod1r op) => eq1.
  move: (CNFb_unique snB mB ax ay eq1) => [<- hb].
  rewrite (cpred_pr2 nB); move:(hb _ lts) => [-> ->].
  split; [apply: succ_nz | exact | exact].
move => k kB Hrec m ey cy mB ay.
have skB:= (BS_succ kB).
move/BnatP: (skB) => p2.
have ok:= proj1 p2.
have osk:= OS_succ ok.
rewrite (succ_of_finite p2) (opow_succ ox ok).
move: (the_CNF_p0(OS_pow ox ok)) => [/CNFB_ax_simp]; rewrite /CNFBv.
set w :=_ ^o _; set ew := Vg _; set cw := Vg _; set m' := P _.
move => [m'B ay'] yv eq1.
move: (Hrec _ _ _ m'B ay' (esym yv)) => [ha hb hc].
move: (cpred_pr m'B ha)=> [m''B mv].
rewrite mv in ay'.
case (ord_zero_dichot oo) => h0.
  move: (CNF_prod_pr6 m''B nB ay' ax h0) => [ax2].
  rewrite - mv yv eq1 => eq2.
  have nmB:= (BS_sum m''B nB).
  rewrite {2 5} mv in eq2.
  move: (CNFb_unique mB (BS_succ nmB) ay ax2 eq2) => [-> h].
  rewrite (cpred_pr2 nmB); move:(h _ (card_lt_succ nmB)) => [-> ->].
  case:(equal_or_not n \0c) => nez.
    by move: (proj2 cnp); rewrite nez h0; case.
  rewrite /cnf_m /cnf_change_n.
  move: (cpred_pr nB nez) => [hu hv].
  have ->: (cpred m' +c n) = m' +c (cpred n).
    by rewrite {1} hv (csum_via_succ _ hu) - (csum_via_succ1 _ m''B) - mv.
  rewrite - mv; Ytac hw; last Ytac0.
    move:(csum_M0le (cpred n) (CS_Bnat m'B)) => hz; co_tac.
  rewrite (csumC m' (cpred n)) (cdiff_pr1 hu m'B).
  rewrite hb (oprod2_succ op ok) - hv.
  split; [apply: succ_nz | exact | exact].
move: (CNF_prod_pr5 m''B nB ay' ax h0) => [ax2].
rewrite - mv yv eq1 => eq2.
move: (CNFb_unique mB snB ay ax2 eq2) => [-> h].
rewrite (cpred_pr2 nB); move:(h _ (card_lt_succ nB)) => [-> ->].
rewrite hb (oprod2_succ op ok).