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

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

Module Ordinals3.

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.

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).
split; [apply: succ_nz | exact | exact].
Qed.

Lemma CNF_pow_pr3 e c n:
   CNFb_axo e c (succ n) -> \0o <o (e n) -> inc n Bnat ->
   (CNFbvo e c (succ n)) ^o omega0 = omega0 ^o ((e n) *o omega0).
Proof.
move=> ax exp nB.
have oo:= OS_omega.
have oen:= (proj32_1 exp).
move:(CNFq_pg4 nB ax) (proj1 (CNFq_pg1 nB (proj1 ax))) => le1 le2.
have pa:= (omega_pow_pos oen).
move:(opow_Mleeq (nesym (proj2 pa)) le1 OS_omega).
move:(opow_Mleeq (nesym (proj2 (ord_lt_leT pa le1))) le2 OS_omega).
rewrite - (opow_prod oo (OS_succ oen) oo) - (opow_prod oo oen oo).
rewrite(indecomp_prod3 exp);apply: ord_leA.
Qed.

Lemma CNF_pow_pr4 ex cx n ey cy m
  (x:=CNFbvo ex cx (succ n)) (y:=CNFbvo ey cy (succ m)):
  CNFb_axo ex cx (succ n) -> \0o <o (ex n) -> inc n Bnat ->
  CNFb_axo ey cy (succ m) -> \0o <o (ey \0o) -> inc m Bnat ->
  x ^o y = omega0 ^o ((ex n) *o y).
Proof.
move=> ax xp nB ayn yp mB.
rewrite /y;move:(CNF_limit mB ayn yp) => [z oz ->].
have ox := OS_CNFb (BS_succ nB) ax.
have oo:= OS_omega.
have op := (proj32_1 xp).
rewrite (opow_prod ox oo oz) (CNF_pow_pr3 ax xp nB).
by rewrite - (opow_prod oo (OS_prod2 op oo) oz) (oprodA op oo oz).
Qed.

Lemma CNF_pow_pr5 x ey cy m (y:=CNFbvo ey cy (succ m)):
  \2o <=o x -> x <o omega0 ->
  CNFb_axo ey cy (succ m) -> \0o <o (ey \0o) -> inc m Bnat ->
  exists z,
   [/\ ordinalp z, y = omega0 *o z & x ^o y = omega0 ^o z].
Proof.
move=> x2 xo ayn tcy mB.
have ox: ordinalp x by ord_tac.
rewrite /y;move: (CNF_limit mB ayn tcy) => [z oz ->].
by rewrite (opow_prod ox OS_omega oz) (opow_int_omega x2 xo); exists z.
Qed.