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

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

Module Ordinals2.

Definition non_coll(p: property) := (~ exists E, forall x, inc x E <-> p x).
Definition ordinal_prop (p:property) := forall x, p x -> ordinalp x.

Lemma unbounded_non_coll (p:property):
  ordinal_prop p ->
  (forall x, ordinalp x -> exists2 y, x <=o y & p y) -> non_coll p.
Proof.
move => op hp [E Ep].
have ose: ordinal_set E by move => x /Ep /op.
move:(hp _ (OS_succ (OS_sup ose))).
move => [y /ord_succ_ltP xy /Ep /(ord_sup_ub ose) h]; ord_tac.
Qed.

Lemma ordinal_not_collectivizing: non_coll ordinalp.
Proof.
apply:unbounded_non_coll => // x ox; exists x => //; ord_tac.
Qed.

Definition ordinal_interval a b := Zo b (fun z => a <=o z).

Lemma ointvP b:
  ordinalp b -> forall a z,
  (inc z (ordinal_interval a b) <-> (a <=o z /\ z <o b)).
Proof.
move => ob a z; split.
  move => /Zo_P [zb ab];split => //; apply /ord_ltP0;split => //; ord_tac.
by move => [az] /ord_ltP0 [pa pb pc]; apply: Zo_i.
Qed.

Lemma ointvP0 b: ordinalp b -> forall z,
 (inc z (ordinal_interval \0o b) <-> z <o b).
Proof.
move=> bb z; apply: (iff_trans (ointvP bb _ _ )).
split; first by case.
by move=> h; split => //; apply: ozero_least; ord_tac.
Qed.

Lemma ointv1 b: ordinalp b -> forall a,
  inc a (ordinal_interval \1o b) <-> (\0o <o a /\ a <o b).
Proof.
move => ob a; split.
 by move /(ointvP ob) => [/ord_ge1P wp1 wp2].
by move => [/ord_ge1P wp1 wp2]; apply /(ointvP ob).
Qed.

Lemma ointv_pr1 b: ordinalp b ->
  ordinal_interval \0o b = b.
Proof.
move=> ob; set_extens t.
  by move /(ointvP0 ob) /ord_ltP0 => [ _ _].
move => tb;apply /(ointvP0 ob) /ord_ltP0;split => //; ord_tac.
Qed.

Lemma ointv_pr2 a b z:
  inc z (ordinal_interval a b) -> ordinalp z.
Proof. move => /Zo_P [p1 p2]; ord_tac. Qed.

Lemma ointv_sup a b: a <o b ->
  \osup (ordinal_interval a b) = \osup b.
Proof.
move => ab.
have ob:ordinalp b by ord_tac.
have aux: sub (ordinal_interval a b) b.
  by move=> t /(ointvP ob) [_] / ord_ltP0 [_ _].
have osb: ordinal_set b by move=> t tb; ord_tac.
apply: (ord_sup_1cofinal) => //; split => // u ub.
have oa: ordinalp a by ord_tac.
have ou: ordinalp u by apply: osb.
case: (ord_le_to_ee oa ou) => aux1.
  exists u; last by ord_tac.
  by apply /(ointvP ob);split => //; apply /ord_ltP0.
exists a => //; apply /(ointvP ob); split => //; ord_tac.
Qed.

Lemma ointv_sup1 a b: a <o b -> limit_ordinal b ->
  \osup (ordinal_interval a b) = b.
Proof.
move=> ab lb; rewrite ointv_sup //.
move: ab lb => [[_ ob _] _].
by move /(limit_ordinal_P1 ob) => [_].
Qed.

Lemma least_ordinal5 x (p: property):
 \0o <o x -> ~(p x) ->
 let y := least_ordinal (fun z => (~ (\0o <o z -> p z))) x in
   [/\ ordinalp y, (\0o <o y), ~(p y) &
    (forall z, inc z (ordinal_interval \1o y) -> p z)].
Proof.
move=> ox px; have orx: ordinalp x by ord_tac.
pose q z := \0o <o z -> p z.
case: (p_or_not_p (q x)); first by move => qx; case: px; apply: qx.
move=> nq; move: (least_ordinal3 orx nq) => /=.
rewrite /q; set y := least_ordinal _ _.
move=> [y1 y2 y3]; split => //.
  by ex_middle h; case: y2.
move=> z /(ointvP y1) [/ord_ge1P z1 z2].
apply: ((y3 _ z2) z1).
Qed.

Definition ofs (f:fterm) := forall x, ordinalp x -> ordinalp (f x).
Definition ofsu (f:fterm) u := forall x, u <=o x -> ordinalp (f x).

Definition sincr_ofsu (f: fterm) u :=
  forall x y, u <=o x -> x <o y -> (f x) <o (f y).
Definition sincr_ofn f x :=
  forall a b, inc a x -> inc b x -> a <o b -> (Vf f a) <o (Vf f b).

Lemma ofs_sincru f u: sincr_ofsu f u -> ofsu f u.
Proof.
move=> pa x ux.
have ox: ordinalp x by ord_tac.
move: (pa _ _ ux (ord_succ_lt ox)) => pb; ord_tac.
Qed.

Lemma ofs_sincr f: sincr_ofs f -> ofs f.
Proof.
move=> pa x ox.
move: (pa _ _ (ord_succ_lt ox)) => pb; ord_tac.
Qed.

Lemma sincr_incr f: sincr_ofs f ->
   (forall x y, x <=o y -> f x <=o f y).
Proof.
move => h x y xy.
case: (equal_or_not x y) => exy; last by exact (proj1 (h _ _ (conj xy exy))).
have ox: ordinalp x by ord_tac.
move: (h _ _ (ord_succ_lt ox)) => [[ax _ _] _].
rewrite - exy; ord_tac.
Qed.

Lemma sincr_ofs_exten f1 f2:
  sincr_ofs f1 -> sincr_ofs f2 ->
  (forall x, ordinalp x -> exists2 y, ordinalp y & f1 x = f2 y) ->
  (forall x, ordinalp x -> exists2 y, ordinalp y & f2 x = f1 y) ->
  f1 =1o f2.
Proof.
move => i1 i2 pa pb x.
apply: (least_ordinal2 (p:= fun z => f1 z = f2 z)) => y oy py.
move: (pa _ oy) => [a oa av]; rewrite av.
case (ord_le_to_ell oa oy); first by move => ->.
  by move => ay; move: (py _ ay); move: (proj2 (i1 _ _ ay)); rewrite av.
move: (pb _ oy) => [c ob bv]; rewrite bv.
case (ord_le_to_ell ob oy); first by move => ->.
  by move => cy; move: (py _ cy) (proj2 (i2 _ _ cy)); rewrite bv => ->.
move => lt1 lt2.
move: (i2 _ _ lt2) (i1 _ _ lt1); rewrite av bv; move => h1 [h2 _]; ord_tac.
Qed.

Definition cont_ofn f x :=
   (forall a, inc a x -> limit_ordinal a ->
      Vf f a = \osup (image_by_fun f a)).

Definition normal_function f x y:=
  [/\ function_prop f x y, sincr_ofn f x & cont_ofn f x].

Definition normal_ofs1 (f: fterm) u:=
  sincr_ofsu f u /\
  (forall X, (forall x, inc x X -> u <=o x) -> nonempty X ->
    \osup (fun_image X f) = f (\osup X)).

Definition normal_ofs2 (f:fterm) u:=
  sincr_ofsu f u /\
  (forall x, limit_ordinal x -> u <o x ->
    f x = \osup (fun_image (ordinal_interval u x) f)).

Definition normal_ofs (f:fterm):=
  sincr_ofs f /\
  (forall x, limit_ordinal x -> f x = \osup (fun_image x f)).

Lemma osum_normal a: ordinalp a -> normal_ofs (fun z => a +o z).
Proof.
move=> oa; split; first by move=> x y xy; apply: osum_Meqlt.
move=> b lb; move: (lb) => [ob iob olbp].
have op: ordinalp (a +o b) by fprops.
have osE: ordinal_set (fun_image b [eta ord_sum2 a]).
  move => x /funI_P [c /(ordinal_hi ob) oc -> ]; fprops.
apply:ord_leA; last first.
  apply:ord_ub_sup => // x /funI_P [z /(ord_ltP ob) xx ->].
  by move: (proj1 (osum_Meqlt xx oa)).
red; split; [exact | by apply:OS_sup | move => w].
rewrite (osum_rec_def oa ob) => h; apply /setU_P.
case /setU2_P:h.
  by move => wa; exists a => //; apply /funI_P;ex_tac; rewrite osum0r.
move /funI_P => [z za zb]; exists (succ_o w); fprops.
move: (ordinal_hi ob za) => oz.
apply /funI_P; exists (succ_o z); [by apply: olbp | rewrite zb - osum2_succ //].
Qed.

Lemma oprod_normal a: \0o <o a -> normal_ofs (fun z => a *o z).
Proof.
move=> ap; split; first by move=> x y xy; apply: oprod_Meqlt.
have oa: ordinalp a by ord_tac.
move=> b lb; move: (lb) => [ob iob olbp].
have op: ordinalp (a *o b) by fprops.
have osE: ordinal_set (fun_image b [eta ord_prod2 a]).
  move => x /funI_P [c /(ordinal_hi ob) oc -> ]; fprops.
apply:ord_leA; last first.
  apply:ord_ub_sup => // x /funI_P [z /(ord_ltP ob) xx ->].
  by move: (proj1 (oprod_Meqlt xx ap)).
red; split; [exact | by apply:OS_sup | move => w ].
rewrite (oprod_rec_def oa ob) => /funI_P [z /setX_P [z1 z2 z3] ->].
move: (olbp _ z3) => z4.
move: (ordinal_hi ob z3) (ordinal_hi ob z4) => o3 o4.
apply /setU_P; exists (a *o (succ_o (Q z))).
  apply /(ord_ltP (OS_prod2 oa o4)); rewrite (oprod2_succ oa o3).
  apply: (osum_Meqlt _ (OS_prod2 oa o3)); ord_tac.
apply/funI_P; ex_tac.
Qed.

Lemma ord_sincr_cont_propu f u:
    (forall x, u <=o x -> f x <o f (succ_o x)) ->
    (forall x, limit_ordinal x -> u <o x ->
      f x = \osup (fun_image (ordinal_interval u x) f)) ->
    sincr_ofsu f u.
Proof.
rewrite /sincr_ofsu;move => h hc x y ux xy.
pose p y := x <o y -> f x <o f y.
apply: (least_ordinal2 (p:= p)) (proj32_1 xy) xy => z sa sc.
case: (limit_ordinal_pr2 sa).
- move => -> ha; case: (ord_lt0 ha).
- move=> [w ow wz]; rewrite wz; move /ord_lt_succP => xw.
  have hx:= (h _ (ord_leT ux xw)).
  case: (equal_or_not x w); [by move => -> | move => xnw ].
  have: w <o z by rewrite wz;apply: ord_succ_lt; apply: OS_succr; ue.
  move /sc => pw; exact: (ord_lt_ltT (pw (conj xw xnw)) hx).
- move => lz xz.
  rewrite (hc z lz (ord_le_ltT ux xz)).
  move /limit_ordinal_P3: lz => [ _ lz].
  move: (lz _ xz) => pa; move: (sc _ pa) => psx.
  move: (ord_succ_lt (proj32 ux)) => hb.
  move: (psx hb) => ha; apply:(ord_lt_leT ha).
  set E := fun_image _ _.
  have: ordinal_set E.
    move => t /funI_P [a /(ointvP sa) [ua az] ->].
    exact: (proj31_1 (h _ ua)).
  move /ord_sup_ub; apply; apply /funI_P; exists (succ_o x) => //.
  apply/ointvP => //; split =>//; apply: (ord_leT ux (proj1 hb)).
Qed.

Lemma ord_sincr_cont_prop f:
    (forall x, ordinalp x -> f x <o f (succ_o x)) ->
    (forall x, limit_ordinal x -> f x = \osup (fun_image x f)) ->
    sincr_ofs f.
Proof.
move => pa pb.
have pa1: (forall x, \0o <=o x -> f x <o f (succ_o x)).
  by move => x [_ ox _]; apply: pa.
have pa2: (forall x, limit_ordinal x ->
     \0o <o x -> f x = union (fun_image (ordinal_interval \0o x) f)).
  move => x lx; move: (lx) => /pb -> _; rewrite ointv_pr1 //;exact:(proj31 lx).
move => x y xy.
exact: (ord_sincr_cont_propu pa1 pa2 (ozero_least (proj31_1 xy)) xy).
Qed.

Lemma ord_sincr_cont_propv f x y: limit_ordinal x -> ordinalp y ->
    function_prop f x y ->
    (forall a, inc a x -> Vf f a <o Vf f (succ_o a)) ->
    cont_ofn f x ->
    normal_function f x y.
Proof.
move => [ox _ lx] oy fpxy pa pb; split => //.
move => a b ax bx ab.
pose p b := a <o b -> inc b x -> Vf f a <o Vf f b.
apply: (least_ordinal2 (p:=p)) (proj32_1 ab) ab bx => z sa sc.
case: (limit_ordinal_pr2 sa).
- move => -> ha; case: (ord_lt0 ha).
- move=> [w ow wz]; rewrite wz; move /ord_lt_succP => xw zx.
  have wx: inc w x by apply: (ordinal_transitive ox zx); fprops.
  have hx:= pa _ wx.
  case: (equal_or_not a w); [by move => -> | move => xnw ].
  have: w <o z by rewrite wz;apply: ord_succ_lt; apply: OS_succr; ue.
  move /sc => pw; exact: (ord_lt_ltT (pw (conj xw xnw) wx) hx).
- move => lz az zx; move: (lz) => [oz _ lz1].
  move: (proj31_1 az) => oa;move: (ord_succ_lt oa) => soa.
  rewrite (pb z zx lz).
  move /limit_ordinal_P3: lz=> [_ lz].
  move: (lz _ az) => pc; apply: (ord_lt_leT (sc _ pc soa (lx _ ax))).
  move: fpxy => [fx sf tf].
  have zz: sub z (source f) by rewrite sf; apply: (ordinal_transitive ox zx).
  apply:ord_sup_ub.
     move => t /(Vf_image_P fx zz) [u uz ->].
     apply: (ordinal_hi oy); rewrite - tf; Wtac.
  apply /(Vf_image_P fx zz); exists (succ_o a) => //; ord_tac.
Qed.

Lemma normal_ofs_equiv f u:
  normal_ofs1 f u <-> normal_ofs2 f u.
Proof.
rewrite /normal_ofs1/ normal_ofs2.
split; move=> [p2 p3]; split => //.
   move=> x lx ux.
   have bx: ordinalp x by ord_tac.
   set X := (ordinal_interval u x).
   have p4: forall x, inc x X -> u <=o x by move=> y /(ointvP bx) [].
   have p5: nonempty X.
     have ou: ordinalp u by ord_tac.
     exists u; apply /ointvP => //; split => //;ord_tac.
   rewrite (p3 _ p4 p5 ) (ointv_sup1 ux lx) //.
move=> X Xp neX.
move: (ofs_sincru p2) => p1.
set Y:= (fun_image X f).
have p4: ordinal_set Y by move=> i /funI_P [z zX ->]; apply: p1; apply: Xp.
have p7: (forall i, inc i X -> ordinalp i).
   by move=>j jX; move: (Xp _ jX)=> [_ ok _].
case: (inc_or_not (union X) X) => sX.
  have sf: inc (f (union X)) Y by apply /funI_P; ex_tac.
  move: (ord_sup_ub p4 sf) => le1.
  have p5: ordinalp (f (union X)) by apply: p1; apply: Xp.
  have p6: (forall i, inc i Y -> i <=o (f (union X))).
    move=> i /funI_P [z zX ->].
    move: (ord_sup_ub p7 zX) => h.
    case: (equal_or_not z (union X)) => h1; first by rewrite h1; ord_tac.
    have h2: z <o (union X) by split.
    by move: (p2 _ _ (Xp _ zX) h2) => [ok _].
  move:(ord_ub_sup p4 p5 p6) => le2; ord_tac.
have aoX: (forall x, inc x X-> ordinalp x).
  by move=> x xX; move: (Xp _ xX);move => [_ ok _ ].
case: (ord_sup_inVlimit aoX neX) => //.
move=> ls.
have [x xX [leux neux]]: exists2 x, inc x X & u <o x.
  move: neX => [y yX]; case: (equal_or_not u y); last first.
    by move => uy; ex_tac; split => //; apply: Xp.
  case: (equal_or_not X (singleton u)) => Xu.
    move: sX; rewrite {1} Xu setU_1 Xu; case; fprops.
  move => h1; rewrite - h1 in yX.
  ex_middle ba; case: Xu; apply: set1_pr => //.
  by move => z zx; ex_middle zu;case:ba;ex_tac; split;[apply: Xp| apply:nesym].
move: (ord_sup_ub aoX xX) => le1.
have ltus: u <o (union X).
  split; [ord_tac | dneg uns; rewrite -uns in le1;ord_tac ].
rewrite (p3 _ ls ltus).
move: (le1) => [_ oos _].
have sXoi: sub X (ordinal_interval u (union X)).
  move=> t tX; apply /(ointvP oos).
  by split; [ apply: Xp | apply: ord_sup_sub].
set Z:= (fun_image _ f).
have sFxoi: sub (fun_image X f) Z.
  by move => t /funI_P [z zX fz]; apply/funI_P; exists z => //; apply: sXoi.
have Zp: (forall z, inc z Z -> ordinalp z).
  by move=> z /funI_P [v /(ointvP oos) [uv _] ->]; apply: p1.
move: (ord_sup_M sFxoi Zp) => h1.
apply: ord_leA => //.
apply: ord_ub_sup => //.
  by apply: OS_sup; move=> i ifi; apply: Zp; apply: sFxoi.
have aux1: ordinalp (union X) by apply: OS_sup.
move=> i /funI_P [z /(ointvP oos) [uz zsX] ->].
have [t tX zt]: exists2 t, inc t X & z <=o t.
  ex_middle h.
  have oz: ordinalp z by move: uz => [_ ok _].
  suff: sub X z by move /(ord_ub_sup1 oz) => h3; ord_tac.
  move=> v vX.
  case: (ord_le_to_el oz (aoX _ vX)) => h3; [case: h; ex_tac | ord_tac ].
have aux: (f t) <=o (union Y).
  apply: ord_sup_ub => //; apply /funI_P; ex_tac.
case: (equal_or_not z t) => ezt; first by ue.
have lzt: z <o t by split.
move: (p2 _ _ uz lzt)=> [aux2 _]; ord_tac.
Qed.

Lemma normal_ofs_equiv1 f:
  normal_ofs1 f \0o <-> normal_ofs f.
Proof.
apply:(iff_trans (normal_ofs_equiv f _)); rewrite /normal_ofs2 /normal_ofs.
split; move=> [h2 h3]; split => //.
- move=> x y xy; apply: h2=> //; apply: ozero_least.
  by move: xy=> [[ox _] _].
- move=> x [pa pb pc].
  rewrite - {2} (ointv_pr1 pa).
  apply: h3 => //; apply /ord_ltP0;split;fprops.
- by move=> x y r1 r2; apply: h2.
- move => x lx wnz.
  have ox: ordinalp x by move: lx =>[ok _].
  by rewrite (ointv_pr1 ox); apply: h3.
Qed.

Lemma normal_ofs_equiv2 f a:
  ordinalp a -> normal_ofs f -> normal_ofs1 f a.
Proof.
move=> oa; move /normal_ofs_equiv1 => [p2 p3]; split => //.
   move=> x y xp yp; apply: p2 =>//; apply: ozero_least; ord_tac.
move=> X xp xX; rewrite p3 //.
move=> t tx; move: (xp _ tx)=> h; apply: ozero_least; ord_tac.
Qed.

Lemma normal_function_incr f a b:
  ordinalp a -> ordinalp b -> normal_function f a b ->
  (forall u v, u <=o v -> v <o a -> Vf f u <=o Vf f v).
Proof.
move => oa ob [[ff sf tf] pa pb] u v uv va.
have ua: u <o a by ord_tac.
have iua: inc u a by ord_tac.
have iva: inc v a by ord_tac.
case: (equal_or_not u v) => nuv.
  have /(ordinal_hi ob) ov : inc (Vf f v) b by Wtac.
  rewrite nuv; ord_tac.
by move:(pa _ _ iua iva (conj uv nuv)) => [].
Qed.

Lemma normal_function_equiv f a b X:
  ordinalp a -> ordinalp b -> normal_function f a b ->
  sub X a -> nonempty X ->
  (\osup X = a \/ Vf f (\osup X) = \osup (image_by_fun f X)).
Proof.
move => oa ob h.
move: (normal_function_incr oa ob h) => incf.
move: h => [[ff sf tf] pa pb] Xa nex.
set y := \osup X.
case: (equal_or_not y a) => eya; [by left | right].
have osx: ordinal_set X by move => t /Xa ta; ord_tac0.
have lya: y <o a by split => //; apply: ord_ub_sup => // x /Xa H; ord_tac.
have iya: inc y a by ord_tac.
have ofy: ordinalp (Vf f y) by apply: (ordinal_hi ob); Wtac.
have Xsf: sub X (source f) by ue.
have osi: ordinal_set (image_by_fun f X).
  move =>t /(Vf_image_P ff Xsf) [u uX ->];apply: (ordinal_hi ob); Wtac.
case: (inc_or_not y X) => iyX.
apply: ord_leA; last first.
  apply:ord_ub_sup => // t /(Vf_image_P ff Xsf) [u uX ->].
  by apply: incf => //; apply: ord_sup_ub.
  apply:ord_sup_ub => //; apply /(Vf_image_P ff Xsf); ex_tac.
case: (ord_sup_inVlimit osx nex); rewrite -/y => // limy.
rewrite (pb _ iya limy).
have ysf: sub y (source f) by rewrite sf; move: lya => [[_ _ h] _].
have Xy: sub X y by move => t tX; move:(ord_sup_sub osx iyX tX) =>h; ord_tac.
symmetry; apply: ord_sup_1cofinal; first split.
- move => t /(Vf_image_P ff Xsf) [u /Xy ux ->]; apply/(Vf_image_P ff ysf).
  ex_tac.
- move => t /(Vf_image_P ff ysf) [u /(ord_ltP (proj31 limy)) uy ->].
  move: (ord_lt_sup osx uy) => [z zx uz].
  have h: inc (Vf f z) (image_by_fun f X) by apply/(Vf_image_P ff Xsf); ex_tac.
  move: (Xa _ zx) => za.
  ex_tac; apply: incf; ord_tac.
- move =>t /(Vf_image_P ff ysf) [u uX ->];apply: (ordinal_hi ob); Wtac.
Qed.

Lemma normal_ofs_uniqueness1 f g (p:fterm) u:
   normal_ofs1 f u -> normal_ofs1 g u -> ordinalp u ->
   (forall x, u <=o x -> f (succ_o x) = p (f x)) ->
   (forall x, u <=o x -> g (succ_o x) = p (g x)) ->
   (f u = g u) ->
  (forall x, u <=o x -> f x = g x).
Proof.
move => [pa pb] [pc pd] ou pe pf pg x cp.
have ox: ordinalp x by ord_tac.
apply: (least_ordinal2 (p:= fun z => u <=o z -> f z = g z)) ox cp => y p1 p3 yp.
case: (equal_or_not u y); [by move <- | move => uny].
have uy: u <o y by [].
case: (limit_ordinal_pr2 p1).
- by move => y0; case: (@ord_lt0 u); rewrite - y0.
- move => [t ot st]; rewrite st; rewrite st in p1.
  have h : u <=o t by apply /ord_lt_succP; rewrite - st.
  move: (ord_succ_lt (proj32 h)); rewrite - {1} st => ty.
  by rewrite (pe _ h) (pf _ h) (p3 _ ty h).
- move => ly.
  set E := ordinal_interval u y.
  have pe1: (forall x, inc x E -> u <=o x) by move => t/(ointvP p1) [].
  have pe2: nonempty E by exists u; apply /(ointvP p1); split => //; ord_tac.
  have pe3: \osup E = y by rewrite (ointv_sup1 uy ly).
  move: (pb _ pe1 pe2) (pd _ pe1 pe2); rewrite pe3 => <- <-.
  apply:ord_sup_2funI => s /(ointvP p1) [s1 s2]; apply: p3 => //; ord_tac1.
Qed.

Lemma normal_ofs_uniqueness f g (p:fterm):
   normal_ofs f -> normal_ofs g ->
   (forall x, ordinalp x -> f (succ_o x) = p (f x)) ->
   (forall x, ordinalp x -> g (succ_o x) = p (g x)) ->
  (f \0o = g \0o) ->
  f =1o g.
Proof.
move => pa pb pc pd pe y oy.
have pa':= (normal_ofs_equiv2 OS0 pa).
have pb':= (normal_ofs_equiv2 OS0 pb).
have pc':(forall x, \0o <=o x -> f (succ_o x) = p (f x)).
  move => x xp; apply: pc; ord_tac.
have pd':(forall x, \0o <=o x -> g (succ_o x) = p (g x)).
  move => x xp; apply: pd; ord_tac.
apply:(normal_ofs_uniqueness1 pa' pb' OS0 pc' pd' pe); ord_tac1.
Qed.

Lemma normal_ofs_existence (p:fterm) a
  (osup := fun y f => \osup (fun_image y (fun z => (p (f z)))))
  (osupp:= fun f => Yo (source f = \0o) a (osup (source f) (Vf f)))
  (f:= fun x => Vf (transfinite_defined (ordinal_o (succ_o x)) osupp) x):
  (forall x, ordinalp x -> x <o p x) ->
  (forall x y, x <=o y -> p x <=o p y) ->
  ordinalp a ->
  [/\ normal_ofs f, f \0o = a &
   (forall x, ordinalp x -> f (succ_o x) = p (f x)) ].
Proof.
move => incrp pi oa.
pose aux b := transfinite_defined (ordinal_o b) osupp.
have frec: forall b, ordinalp b ->
     [/\ function (aux b), source (aux b) = b,
       (inc \0o b -> Vf (aux b) \0o = a) &
       (forall y, inc y b -> y <> \0o ->
         Vf (aux b) y = osup y (Vf (aux b)))].
  move=> b ob.
  move: (transfinite_defined_pr osupp (ordinal_o_wor ob)).
  rewrite /transfinite_def (ordinal_o_sr b) //.
  have sh: forall c, inc c b -> source
    (restriction_to_segment (ordinal_o b) c
      (transfinite_defined (ordinal_o b) osupp)) = c.
    move=> c cb; rewrite /restriction_to_segment /restriction1; aw.
    apply: ordinal_segment => //.
  move=> [[h1 _] h2 h3]; split => //.
    by move=> zb;rewrite (h3 _ zb); rewrite /osupp Y_true //; apply: sh.
  move => y xb l4; rewrite (h3 _ xb); move: (sh _ xb) => sh1.
  rewrite /osupp /osup sh1; Ytac0; congr union.
  have oy: ordinalp y by ord_tac.
  have aux1: forall z, inc z y ->
   Vf (aux b) z = Vf (restriction_to_segment (ordinal_o b) y
              (transfinite_defined (ordinal_o b) osupp)) z.
    move=> z zy.
    have lt1: glt (ordinal_o b) z y.
      apply /ordo_ltP => //; apply: (ordinal_transitive ob xb zy).
    rewrite restriction1_V //;last by apply /segmentP.
    rewrite h2 - {2} (ordinal_o_sr b); apply: sub_segment.
  by set_extens t; move /funI_P => [z z1 z2]; apply /funI_P;
       ex_tac; rewrite z2 (aux1 _ z1) //.
have frec2: forall b1 b2 x, ordinalp b1 -> ordinalp b2 ->
     inc x b1 -> inc x b2 -> Vf (aux b1) x = Vf (aux b2) x.
  move => b1 b2 x ob1 ob2.
  pose q z := inc z b1 -> inc z b2 -> Vf (aux b1) z = Vf (aux b2) z.
  move => xb1; move: (ordinal_hi ob1 xb1) => x1; move: xb1.
  apply:(least_ordinal2 (p:=q)) => // z oz zp2 tb1 tb2.
  move: (frec _ ob1) => [_ _ h0 hg].
  move: (frec _ ob2) => [_ _ h0' hg'].
  case: (equal_or_not z \0o) => ez0; first by rewrite ez0 h0 ?h0'//;ue.
  rewrite (hg _ tb1 ez0) (hg' _ tb2 ez0); apply: ord_sup_2funI => t tz.
  have ltwz: t <o z by apply /ord_ltP.
  have zb1: inc t b1 by exact: (ordinal_transitive ob1 tb1 tz).
  have zb2: inc t b2 by exact: (ordinal_transitive ob2 tb2 tz).
  rewrite ((zp2 t ltwz) zb1 zb2) //.
have f0: f \0o = a.
   move: (frec _ OS1) => [_ _]; rewrite - succ_o_zero -/(f _) => h _.
   apply: h; fprops.
have frec3: forall y, \0o <o y -> f y = osup y f.
  move=> y yp.
  have oy: ordinalp y by ord_tac.
  have ob: ordinalp (succ_o y) by fprops.
  have ynz: y <> \0o by move: yp => [_ h]; apply: nesym.
  have iyb: inc y (succ_o y) by rewrite /succ_o; fprops.
  move: (frec _ ob) => [_ _ h0 hg]; rewrite {1} /f (hg _ iyb ynz) /osup.
  suff A: forall t, inc t y ->
     Vf (aux (succ_o y)) t = Vf (aux (succ_o t)) t.
     congr union; set_extens t; move => /funI_P [w z1 z2]; apply /funI_P;
       ex_tac; rewrite z2 (A _ z1) //.
  move => t ty; apply: frec2 => //; [apply:OS_succ; ord_tac | | fprops].
  rewrite /succ_o; fprops.
have frec4: forall x, ordinalp x -> ordinalp (f x).
   move => x; apply:(least_ordinal2 (p:=fun z => ordinalp (f z))) => z oz zp2.
   case: (equal_or_not z \0o) => zp; first by rewrite zp f0.
   rewrite (frec3 _ (ord_ne0_pos oz zp)); apply:OS_sup.
   move => t /funI_P [u /(ord_ltP oz) /zp2 /incrp h ->]; ord_tac.
have frec5: forall x y, x <o y -> p (f x) <=o f y.
  move => x y xy.
  have oz: ordinalp y by ord_tac.
  have ixy: inc x y by apply /ord_ltP.
  have yp: \0o <o y by apply:ord_ne_pos => //; ex_tac.
  rewrite (frec3 _ yp) /osup; apply: ord_sup_ub; last by apply /funI_P; ex_tac.
  move => t /funI_P [z /(ordinal_hi oz) /frec4 /incrp h ->]; ord_tac.
have frec6: forall x y, x <o y -> (f x) <o f y.
  move => x y xy; move: (frec5 _ _ xy) => l1.
  move: (incrp _ (frec4 _ (proj31_1 xy))) => l2; ord_tac.
have frec7:forall x, ordinalp x -> f (succ_o x) = p (f x).
  move => x ox.
  have xsx: x <o succ_o x by apply: ord_succ_lt.
  apply: ord_leA; last by apply: (frec5 _ _ xsx).
  move: (OS_succ ox) => osx.
  have sxp: \0o <o succ_o x by apply /ord_lt_succP; apply: ozero_least.
  rewrite (frec3 _ sxp) /osup;apply: ord_ub_sup.
  - move => t /funI_P [z /(ordinal_hi osx) /frec4 /incrp h ->]; ord_tac.
  - move: (incrp _ (frec4 _ ox)) => h; ord_tac.
  - move => t /funI_P [z zx ->]; apply: pi.
    case/setU1_P: zx; last by move ->; move: (frec4 _ ox) =>h; ord_tac.
    by move /(ord_ltP ox) => /frec6 [].
split => //; split =>// x lx; move:(proj31 lx) => ox.
rewrite (frec3 _ (limit_positive lx)) /osup.
have hz: forall z, inc z x -> z <o succ_o z.
  move => z zx ;apply: ord_succ_lt; ord_tac.
apply: ord_sup_2cofinal;split; move => c /funI_P [z zx ->]; move:(hz _ zx)=> ht.
  move:(proj33 lx _ zx) => h; exists (f (succ_o z)); last by apply:frec5.
  apply /funI_P; ex_tac.
exists (f (succ_o z)); first by apply/funI_P; ex_tac; apply: frec7; ord_tac.
by move: (frec6 _ _ ht) => [].
Qed.

Lemma normal_ofs_limit1 f u x: normal_ofs1 f u -> u <o x -> limit_ordinal x ->
  limit_ordinal (f x).
Proof.
move=> /normal_ofs_equiv [pa pb] cux lx.
rewrite (pb _ lx cux); move/limit_ordinal_P3: (lx) => [[[_ ox _] _] pd].
have ov := (ofs_sincru pa).
set E := (fun_image (ordinal_interval u x) f).
have ou: ordinalp u by ord_tac.
have uu: inc u (ordinal_interval u x) by apply/(ointvP ox);split=> //;ord_tac.
have oe: ordinal_set E.
  by move=> t /funI_P [z /(ointvP ox) [uz _] ->]; apply: ov.
have ne: nonempty E by rewrite /E;exists (f u); apply /funI_P;ex_tac.
case: (ord_sup_inVlimit oe ne) => //.
move=> /funI_P [z /(ointvP ox) [sa /pd sb] fz].
have lt1:= (ord_succ_lt (proj32 sa)).
have se: inc (f (succ_o z)) E.
  apply /funI_P; exists (succ_o z)=> //;apply /(ointvP ox).
  split => //;exact (ord_leT sa (proj1 lt1)).
move: (ord_sup_ub oe se); rewrite fz => l1.
move: (pa z (succ_o z) sa lt1) => l2; ord_tac.
Qed.

Lemma normal_ofs_limit f x: normal_ofs f -> limit_ordinal x ->
  limit_ordinal (f x).
Proof.
move => /(normal_ofs_equiv2 OS0) nf lx; apply:(normal_ofs_limit1 nf _ lx).
by apply: limit_positive.
Qed.

Lemma normal_ofs_compose1 f fb g gb:
 ordinalp fb -> ordinalp gb -> fb <=o g gb ->
 normal_ofs1 f fb -> normal_ofs1 g gb -> normal_ofs1 (f \o g) gb.
Proof.
move => ofb ogb le1 [sa pa] [sb pb].
have aux: forall z, gb <=o z -> fb <=o g z.
  move => z zh; apply: (ord_leT le1).
  move: (ofs_sincru sb zh)=> oug.
  case: (equal_or_not gb z); [move ->;ord_tac | move =>h].
  exact (proj1 (sb gb z (ord_leR ogb) (conj zh h))).
split.
  move => u v ha uv /=.
  by move: (sb _ _ ha uv); apply: sa; apply: aux.
move => X Xp neX /=; rewrite - (pb _ Xp neX).
set Y := (fun_image X g).
have sc:(forall x, inc x Y -> fb <=o x).
  by move => x /funI_P [z /Xp zx ->]; apply: aux.
have nY: nonempty Y by move: neX => [t tX]; exists (g t); apply /funI_P; ex_tac.
rewrite -(pa _ sc nY); congr union; set_extens t; move/funI_P => [z za ->].
  apply/funI_P; exists (g z)=> //;apply /funI_P; ex_tac.
move/funI_P: za => [u tX ->]; apply/funI_P; ex_tac.
Qed.

Lemma normal_ofs_compose f g:
 normal_ofs f -> normal_ofs g -> normal_ofs (f \o g).
Proof.
move => /(normal_ofs_equiv2 OS0) pa /(normal_ofs_equiv2 OS0) pb.
have h := ozero_least (ofs_sincru (proj1 pb) (ord_leR OS0)).
by move:(normal_ofs_compose1 OS0 OS0 h pa pb) => /normal_ofs_equiv1.
Qed.

Lemma osum_limit x y: ordinalp x -> limit_ordinal y ->
  limit_ordinal (x +o y).
Proof.
by move=> ox ly; apply:normal_ofs_limit=> //; apply: osum_normal.
Qed.

Lemma oprod_limit x y: \0o <o x -> limit_ordinal y ->
  limit_ordinal (x *o y).
Proof. by move=> ox ly; apply:normal_ofs_limit=> //; apply: oprod_normal. Qed.

Lemma osi_gex x f: sincr_ofs f -> ordinalp x -> x <=o (f x).
Proof.
move=> finc ox.
case: (ord_le_to_el ox (ofs_sincr finc ox)) => // lt1.
move: (least_ordinal4 ox lt1 (p:=fun z => f z <o z)) => [pd pb pc].
move: (finc _ _ pb) => ha.
move: (pc _ (proj32_1 ha) ha) => lt2; ord_tac.
Qed.

Lemma odiff_normal a: ordinalp a -> normal_ofs1 (ord_diff ^~ a) a.
Proof.
move => oa; apply/normal_ofs_equiv.
have aux1:forall u v, a <=o u -> u <o v -> u -o a <o v -o a.
  move => u v au uv; move: (ord_leT au (proj1 uv)) => av.
  move: (odiff_pr au) (odiff_pr av) => [ou e1] [ov e2].
  by move: uv; rewrite {1} e1 {1} e2; move /(osum_Meqltr ou ov oa).
have aux:forall u v, a <=o u -> u <=o v -> u -o a <=o v -o a.
  move => u v au uv; move: (ord_leT au uv) => av.
  move: (odiff_pr au) (odiff_pr av) => [ou e1] [ov e2].
  by move: uv; rewrite {1} e1 {1} e2; move /(osum_Meqler ou ov oa).
split => //.
move => x lx ax.
have ox:= (proj31 lx).
set E := fun_image _ _.
have ose: ordinal_set E.
  by move => t /funI_P [v /(ointvP ox) [[_ ov _] vx] -> ]; apply: OS_diff.
have m1: ordinal_ub E (x -o a).
  by move => t /funI_P [v /(ointvP ox) [av [vx _]] -> ]; apply: aux.
move: (odiff_pr (proj1 ax)) => [sa sb].
have os:= (OS_sup ose).
move:(ord_ub_sup ose sa m1) => le1.
case: (ord_le_to_el sa os) => le2; first by ord_tac.
move: (osum_Meqlt le2 oa); rewrite - sb => eq1.
have: inc (\osup E) E.
  apply /funI_P;exists (a +o \osup E); last by symmetry; apply: odiff_pr1.
  by apply/(ointvP ox); split => //; apply:osum_Mle0.
move => /funI_P [y /(ointvP ox) [e1 e2] eq].
move/(limit_ordinal_P3): (lx) => [ _ h3]; move: (h3 _ e2) => h4.
have h5 :=(ord_succ_lt (proj32 e1)).
move: (aux1 _ _ e1 h5) => h6.
have se: (inc ((succ_o y) -o a) E).
   apply/funI_P; exists (succ_o y) => //; apply/(ointvP ox); split => //.
   move: (proj1 h5) => e3; ord_tac.
move: (ord_sup_ub ose se); rewrite eq => h7; ord_tac.
Qed.

Lemma normal_shift f a: normal_ofs f -> ordinalp a ->
  normal_ofs (fun z => (f(a +o z) -o a)).
Proof.
move => sa oa.
move: (normal_ofs_compose sa (osum_normal oa)) => sb.
move: (odiff_normal oa) => sc.
set f1 := (ord_diff^~ a); set f2:= (f \o [eta ord_sum2 a]).
have h1: a <=o f2 \0o.
 rewrite /f2 /= (osum0r oa); exact: (osi_gex (proj1 sa) oa).
move/normal_ofs_equiv1: sb => sb'; apply/normal_ofs_equiv1.
exact:(normal_ofs_compose1 oa OS0 h1 sc sb').
Qed.

Lemma osi_gexu f u t x:
  sincr_ofsu f u -> u <=o t -> t <=o f t -> t <=o x ->
   x <=o (f x).
Proof.
move=> finc ut tft tx.
have ox: ordinalp x by ord_tac.
case: (ord_le_to_el ox (ofs_sincru finc (ord_leT ut tx))) => // lt1.
pose p x := t <=o x /\ f x <o x.
move: (least_ordinal4 ox (conj tx lt1) (p:=p)) => [pd [pb1 pb2] pc].
set y := least_ordinal p x.
case: (equal_or_not t y) => ty.
  by move: pb2; rewrite -/y - ty => h; ord_tac.
move: (ord_leT tft (proj1 (finc t y ut (conj pb1 ty)))) => pa.
have ofy: ordinalp (f y) by ord_tac.
move: (pc _ ofy (conj pa (finc (f y) y (ord_leT ut pa) pb2))) => h; ord_tac.
Qed.

Lemma normal_fn_unbounded f a x:
  normal_function f a a -> x<o a -> x <=o (Vf f x) /\ Vf f x <o a.
Proof.
 move=> [[ff sf tf] finc _] laxx.
have oa: ordinalp a by ord_tac.
have ox: ordinalp x by ord_tac.
have xsf: inc x a by apply /(ord_ltP oa).
have ft: inc (Vf f x) a by Wtac.
split; last by apply /(ord_ltP oa).
have ofx:= (ordinal_hi oa ft).
case: (ord_le_to_el ox ofx) => // lt1.
pose p z := z <o a /\ Vf f z <o z.
have px: p x by done.
move: (least_ordinal4 ox px) => [pc [pd pe] pf].
move: (ord_le_ltT (proj1 pe) pd) => a2.
move /(ord_ltP oa): pd => a1.
move /(ord_ltP oa): (a2) => a3.
move: (finc _ _ a3 a1 pe) => ha.
have hb: p (Vf f (least_ordinal p x)) by [].
move: (pf _ (proj32_1 ha) hb) => lt2; ord_tac.
Qed.

Lemma osum_increasing5 a w: ordinalp a ->
  (sincr_ofsu w a) ->
  ((forall x y, a <=o x -> ordinalp y -> (w (x) +o y) <=o w (x +o y))
  /\ (exists2 b, a <=o b & forall x, b <=o x -> x <=o w (x))).
Proof.
move=> oa h.
have osw:= (ofs_sincru h).
have pr1: forall x y, a <=o x -> ordinalp y -> (w x +o y) <=o w (x +o y).
  move=> x y ax oy; have ox: ordinalp x by ord_tac.
  apply:(least_ordinal2 (p:= fun z => (w x +o z) <=o w (x +o z))) oy => z oz hr.
  move: (osw _ ax) => owx.
  have pa: forall t, ordinalp t -> a <=o (x +o t).
    move=> t ot;move: (osum_Mle0 ox ot) => h2; ord_tac.
  case: (limit_ordinal_pr2 oz).
  - move=> ->; rewrite (osum0r ox)(osum0r owx); ord_tac.
  - move=> [t ot uv].
    move: (ord_succ_lt ot); rewrite -uv => h1; move: (hr _ h1) => le1.
    move: (h _ _ (pa _ ot) (osum_Meqlt h1 ox)) => lt1.
    rewrite {1} uv - (osum2_succ owx ot); apply /ord_succ_ltP; ord_tac.
  - move: (osum_normal owx) => [_ opn].
    move=> lz; rewrite (opn _ lz).
    apply: ord_ub_sup.
      move => t /funI_P [tu uz ->]; apply: OS_sum2 => //; ord_tac0.
    by apply: osw; apply: pa.
  move=> i /funI_P[j jz ->].
  have ljz: j <o z by apply /ord_ltP.
  move: (hr _ ljz) => le1.
  move: (h _ _ (pa _ (proj31_1 ljz)) (osum_Meqlt ljz ox)) => [ lt1 _]; ord_tac.
split; first by exact;move=> a w oa h1.
set b:= succ_o a.
have ob: ordinalp b by apply: OS_succ.
move: (ord_succ_lt oa); rewrite -/b; move => [leab _].
set c := b *o omega0.
have ab:= (ord_leT leab (oprod_Mle1 ob ord_lt_0omega)).
exists c; first by exact.
suff bv: c <=o w c.
  move => x xc; apply: (osi_gexu h ab bv xc).
have bp: \0o <o b by apply:ord_ne_pos => //; exists a; rewrite /b; fprops.
move: (oprod_normal bp) => [_ aux].
move: (aux _ omega_limit); rewrite - /c => e1; rewrite {1} e1.
have owc: ordinalp (w c) by apply:osw.
have H: forall z, inc z omega0 -> ordinalp (b *o z).
   move => z zo;exact (OS_prod2 ob (ordinal_hi OS_omega zo)).
apply: ord_ub_sup => // t /funI_P[z zo ->]; move:(H _ zo) => obz //.
have owb: ordinalp (w b) by apply: osw.
have oz := (ordinal_hi OS_omega zo).
have le1: b *o z <=o (w b +o (b *o z)) by apply: osum_M0le.
move: (pr1 _ _ leab obz).
rewrite (osum_x_xy ob oz).
set n:= (\1o +o z) => le2.
move: (ord_leT le1 le2) => le3.
suff le4: w (b *o n) <=o w (b *o omega0) by ord_tac.
case: (equal_or_not (b *o n) (b *o omega0)) => sv.
   rewrite sv; apply: ord_leR; by apply: osw.
have [ltno _]: n <o omega0.
   move: BS1=> b1; apply/ (ord_ltP OS_omega); rewrite/n osum2_2int //; fprops.
move: (oprod_Meqle ltno ob) => le4.
have lt1:(b *o n) <o (b *o omega0) by split.
have le5: a <=o (b *o n).
  rewrite /n -(osum_x_xy ob oz); apply: (ord_leT leab).
  by apply: osum_Mle0.
by move: (h _ _ le5 lt1) => [ok _].
Qed.

Lemma osi_gex1 x f:
   sincr_ofs f -> ordinalp x -> exists y,
      [/\ ordinalp y, x <=o (f y) &
        forall z, ordinalp z -> x <=o (f z) -> y <=o z].
Proof.
move=> finc ox.
move: (osi_gex finc ox) => lxy.
pose p y := x <=o (f y).
move: (@least_ordinal4 x p ox lxy) => [pa pb pc].
exists (least_ordinal p x);split => //.
Qed.

Lemma normal_ofs_bounded x f: ordinalp x -> normal_ofs f ->
  x <o f \0o \/ exists y, [/\ ordinalp y, f y <=o x & x <o f (succ_o y)].
Proof.
move=> ox [pa pb].
move: (osi_gex1 pa ox) => [y [oy xle ymin]].
case: (equal_or_not x (f y)) => xo.
  move: (pa _ _ (ord_succ_lt oy)) => lt1.
  rewrite xo;right; exists y; split => //; apply: ord_leR; ord_tac.
have xlt: x <o f y by split.
case: (limit_ordinal_pr2 oy).
    by move => ye; move: xlt; rewrite ye => xx; left.
  move => [z oz yz]; rewrite yz in oy.
  right; exists z; rewrite -yz;split => //.
  move: (ord_succ_lt oz); rewrite -yz => le3.
  move: (pa _ _ le3) => [[ofz _] _].
  case: (ord_le_to_ee ofz ox) => //.
  move=> le1; move: (ymin _ oz le1) => le2; ord_tac.
move => li; move: xlt; rewrite (pb _ li) => xu.
have os: ordinal_set (fun_image y f).
  move=> t /funI_P [z zy ->]; move: (ordinal_hi oy zy) => oz.
  exact: (ofs_sincr pa oz).
move: (ord_lt_sup os xu) => [z /funI_P [t ty ->] le2].
have yt: t <o y by apply /(ord_ltP oy).
move:(ymin _ (ordinal_hi oy ty) (proj1 le2)) => yt'; ord_tac.
Qed.

Definition least_fixedpoint_ge f x y:=
 [/\ x <=o y, f y = y & (forall z, x <=o z -> f z = z -> y <=o z)].
Definition the_least_fixedpoint_ge f x :=
  (\osup (target (induction_defined f x))).

Definition fixpoints f := Zo (source f) (fun z => Vf f z = z).

Lemma normal_ofs_fix1 f u x:
  normal_ofs1 f u -> u <=o x -> x <=o f x ->
  least_fixedpoint_ge f x (the_least_fixedpoint_ge f x).
Proof.
move=> nf0 ux xfx; rewrite /the_least_fixedpoint_ge.
have ox: ordinalp x by ord_tac.
move: nf0 => [sif nf].
have aux: forall t, x <=o t -> t <=o f t.
  by move => t; apply:(osi_gexu sif ux xfx).
move: (induction_defined_pr f x).
set g := induction_defined f x; move=> [sg sjg gz gnz].
have fg: function g by fct_tac.
set y := \osup (target g).
have pb: forall i, inc i (target g) -> x <=o i.
   move=> i itg; move: ((proj2 sjg) _ itg) => [j jsg <-].
   move: j jsg; rewrite sg; apply: cardinal_c_induction.
     rewrite gz; ord_tac.
   move=> n nB; rewrite (gnz _ nB) => p1.
   move: (aux _ p1) => h; ord_tac.
have pc: (forall i, inc i (target g) -> u <=o i).
   move=> i itg; move: (pb _ itg)=> le2; ord_tac.
have xi: inc x (target g) by rewrite -gz; Wtac; rewrite sg; fprops.
have ne: nonempty (target g) by exists x.
have otg: ordinal_set (target g).
  move=> t tg; move: (pb _ tg) => le; ord_tac.
split => //.
- by apply:(ord_sup_ub otg xi).
- rewrite - (nf _ pc ne).
  apply: ord_sup_1cofinal; [ split | done].
    move => t /funI_P [z ztg ->].
    move: ((proj2 sjg) _ ztg) => [i isg <-].
    rewrite sg in isg; rewrite -gnz //; Wtac;rewrite sg; fprops.
  move=> a atg.
  move: ((proj2 sjg) _ atg) => [i isg <-].
  rewrite sg in isg.
  have wt: inc (Vf g i) (target g) by Wtac.
  exists (Vf g (succ i)); rewrite (gnz _ isg).
     by apply /funI_P; exists (Vf g i).
  by apply: aux; apply: pb.
- move => z xz fz.
  have oz: ordinalp z by ord_tac.
  apply: ord_ub_sup => //.
  move=> i itg; move: ((proj2 sjg) _ itg) => [j jsg <-].
  move: j jsg; rewrite sg; apply: cardinal_c_induction; first by rewrite gz.
  move=> n nB; rewrite (gnz _ nB) => p1.
  have /pc le1: inc (Vf g n) (target g) by Wtac.
  case: (equal_or_not (Vf g n) z) => h; first by rewrite h fz; ord_tac.
  rewrite - fz; exact: (proj1 (sif _ _ le1 (conj p1 h))).
Qed.

Lemma normal_ofs_fix x f:
  normal_ofs f -> ordinalp x ->
  least_fixedpoint_ge f x (the_least_fixedpoint_ge f x).
Proof.
move => nf ox.
move/normal_ofs_equiv1:(nf)=> nf1; apply: (normal_ofs_fix1 nf1).
  ord_tac1.
exact:(osi_gex (proj1 nf) ox).
Qed.

Lemma normal_function_fix f a x
  (y:= the_least_fixedpoint_ge (Vf f) x):
  normal_function f a a -> x <o a ->
  (y = a \/
  [/\ x <=o y, y <o a, Vf f y = y &
    (forall z, x <=o z -> z <o a -> Vf f z = z -> y <=o z)]).
Proof.
move=> nf lxa.
have aux: forall x, x <o a -> x <=o (Vf f x) /\ Vf f x <o a.
  by move => t ta; apply: normal_fn_unbounded.
have ox: ordinalp x by ord_tac.
have oa: ordinalp a by ord_tac.
move: (induction_defined_pr (Vf f) x).
set g := induction_defined (Vf f) x; move=> [sg sjg gz gnz].
have fg: function g by fct_tac.
move: (nf) => [[ff sf tf] sif nf0].
have pb: forall i, inc i (target g) -> x <=o i /\ i <o a.
   move=> i itg; move: ((proj2 sjg) _ itg) => [j jsg <-].
   move: j jsg; rewrite sg; apply: cardinal_c_induction.
     rewrite gz; split => //;ord_tac.
   move=> n nB; rewrite (gnz _ nB); move => [p1 p2].
   move: (aux _ p2) => [s1 s2]; split => //; ord_tac.
have osg: ordinal_set (target g) by move => i /pb [_] ia;ord_tac.
have sta: sub (target g) a by move => t /pb [_] h; ord_tac.
have netg: nonempty (target g) by exists (Vf g \0c); Wtac; rewrite sg; fprops.
have sa: x <=o y.
  apply :ord_sup_ub => //; rewrite - /g - gz; Wtac; rewrite sg; fprops.
have sb: y <=o a by apply :ord_ub_sup => // i /pb [_ []].
case: (equal_or_not y a) => eya; [by left | right;split => //; last first].
   move => z xz za fz.
   have oz: ordinalp z by ord_tac.
   apply: ord_ub_sup => //.
   move=> i itg; move: ((proj2 sjg) _ itg) => [j jsg <-].
   move: j jsg; rewrite sg; apply: cardinal_c_induction; first by rewrite gz.
   move=> n nB; rewrite (gnz _ nB) => p1; rewrite - fz.
   case: (equal_or_not ( Vf g n) z) => neq; first by rewrite neq fz; ord_tac.
   have ha: inc (Vf g n) a by apply /(ord_ltP oa); ord_tac.
   have hb: inc z a by ord_tac.
   exact (proj1(sif (Vf g n) z ha hb (conj p1 neq))).
move: (aux _ (conj sb eya)) => [sc sd].
apply: ord_leA => //.
move: (sta); rewrite - sf => stf.
have ha: ordinal_set (image_by_fun f (target g)).
  move => t /(Vf_image_P ff stf) [u /pb [_ /aux [_ h]] ->]; ord_tac.
case: (normal_function_equiv oa oa nf sta netg) => //; rewrite -/y => ->.
apply: ord_ub_sup => //; first by ord_tac.
move => t /(Vf_image_P ff stf) [u utg ->].
move: (proj2 sjg _ utg)=> [v va <- ].
rewrite sg in va; rewrite - (gnz _ va); apply :ord_sup_ub => //.
rewrite -/g; Wtac; rewrite sg; fprops.
Qed.

Lemma next_fix_point_small f C (E:= succ_c C): infinite_c C ->
  normal_ofs f ->
  (forall x, inc x E -> inc (f x) E) ->
  (forall x, inc x E -> inc (the_least_fixedpoint_ge f x) E).
Proof.
move => icE nf fee.
move: (succ_c_pr1 (proj1 icE)) => [pa pb pc].
move => x xE.
move: (induction_defined_pr f x) => [qa qb qc qd].
move: (image_smaller_cardinal (proj1 qb));rewrite qa (surjective_pr0 qb)=> sa.
apply: succ_c_sup => //.
  by apply: (card_leT sa); rewrite cardinal_Bnat; apply /infinite_c_P2.
move => t /(proj2 qb); rewrite qa; move => [z zB <-]; move: z zB.
apply: cardinal_c_induction; first by rewrite qc.
move => n nB /fee hr; rewrite qd //.
Qed.

Lemma next_fix_point_small1 f C x (E:= succ_c C)
  (y:= the_least_fixedpoint_ge (Vf f) x):
  infinite_c C -> normal_function f E E -> inc x E ->
   [/\ x <=o y, inc y E, Vf f y = y &
    (forall z, x <=o z -> inc z E -> Vf f z = z -> y <=o z)].
Proof.
move => icE nf xE.
move: (succ_c_pr1 (proj1 icE)) => [pa pb pc].
move: (induction_defined_pr (Vf f) x) => [qa qb qc qd].
move: (image_smaller_cardinal (proj1 qb));rewrite qa (surjective_pr0 qb)=> sa.
have fee: (forall x, inc x E -> inc (Vf f x) E).
  move:nf => [[ff sf tf] pd pe].
  rewrite -{1} sf - tf => t tsf; Wtac.
have ye: inc y E.
  apply: succ_c_sup => //.
    by apply: (card_leT sa); rewrite cardinal_Bnat; apply /infinite_c_P2.
  move => t /(proj2 qb); rewrite qa; move => [z zB <-]; move: z zB.
  apply: cardinal_c_induction; first by rewrite qc.
  move => n nB /fee hr; rewrite qd //.
have [oe _] := (pa).
have xe: x <o E by apply/ord_ltP=> //.
case: (normal_function_fix nf xe); rewrite -/y.
  by move => yee; move:ye; rewrite yee; move: (ordinal_irreflexive oe).
by move => [ta tb tc td]; split => // z xz ze; apply: td => //; apply/ord_ltP.
Qed.

Lemma normal_fix_cofinal C (E := succ_c C) f:
   infinite_c C -> normal_function f E E ->
   ord_cofinal (fixpoints f) E.
Proof.
move => icE nf.
move: (nf) => [[ff sf tf] _ _].
split; first by rewrite - sf; apply: Zo_S.
move => x xE.
move: (next_fix_point_small1 icE nf xE); rewrite -/E - sf.
set y := the_least_fixedpoint_ge (Vf f) x; move => [pa pb pc pd].
by exists y => //; apply/Zo_P.
Qed.

Lemma big_ofs
  (p:= fun z => succ_c (cardinal z))
  (osup := fun y f => \osup (fun_image y (fun z => (p (f z)))))
  (osupp:= fun f => Yo (source f = \0o) \0o (osup (source f) (Vf f)))
  (f:= fun x => Vf (transfinite_defined (ordinal_o (succ_o x)) osupp) x):
  [/\ normal_ofs f, f \0o = \0o,
   (forall x, ordinalp x -> f (succ_o x) = p (f x))&
   forall C, infinite_c C ->
       exists x, inc x (succ_c C) /\ ~ (inc (f x) (succ_c C)) ].
Proof.
have sa: (forall x, ordinalp x -> x <o p x).
  move => x ox; rewrite /p.
  have pc: cardinalp (cardinal x) by fprops.
  have pa: cardinalp (succ_c (cardinal x)) by apply: CS_succ_c.
  apply /(ord_ltP (proj1 pa)); apply /(succ_cP pc); split; fprops.
have sb: (forall x y : Set, x <=o y -> p x <=o p y).
  move => x y xy; rewrite /p.
  move:(ordinal_cardinal_le1 xy) => h.
  by apply:ordinal_cardinal_le; apply:succ_c_pr6.
move: (normal_ofs_existence sa sb OS0).
rewrite -/osup -/osupp -/f.
move => [pa pb pc]; split => //.
move => c ic; exists (succ_o c).
move: (proj1 ic) => cc; move: (proj1 cc) => oc.
move: (CS_succ_c cc)=> cs.
have oso: ordinalp (succ_o c) by move: cc=> [co _];apply:OS_succ.
split.
   have os1 := OS1.
   apply /(succ_cP cc); split => //.
   rewrite - ord_succ_pr // osum_cardinal // (card_card cc) sum2_infinite //.
     fprops.
   rewrite (card_card CS1); apply: finite_le_infinite => //; fprops.
have eq1: (f (succ_o c)) = p (f c) by apply: pc.
move /(succ_cP cc)=> [sc sd].
have se: c <=o (f c) by apply: (osi_gex (proj1 pa) oc).
have: p c <=o p (f c) by apply: sb.
move /ordinal_cardinal_le1; rewrite - eq1 /p (card_card cc).
rewrite (card_card cs) => h.
move: (card_leT h sd); move: (succ_c_pr2 cc) => ra rb; co_tac.
Qed.

Definition omax x y:= Yo (x <=o y) y x.

Lemma OS_omax x y: ordinalp x -> ordinalp y -> ordinalp(omax x y).
Proof. by move => ox oy; rewrite /omax;Ytac w. Qed.

Lemma omaxC x y: ordinalp x -> ordinalp y -> omax x y = omax y x.
Proof.
rewrite /omax => ox oy.
case: (ord_le_to_ell ox oy).
+ by move: (ord_leR oy) =>h; move => ->; Ytac0.
+ move => xy; move: (proj1 xy) => h1; Ytac0; Ytac w => //; ord_tac.
+ move => xy; move: (proj1 xy) => h1; Ytac0; Ytac w => //; ord_tac.
Qed.

Lemma omaxA x y z: ordinalp x -> ordinalp y -> ordinalp z ->
    omax x (omax y z) = omax (omax x y) z.
Proof.
move =>ox oy oz.
rewrite /omax.
case: (ord_le_to_el ox oy) => h1.
   Ytac0.
   case: (ord_le_to_el oy oz) => h2.
     by move: (ord_leT h1 h2) => h3; Ytac0; Ytac0.
   by case : (p_or_not_p (y <=o z)) => h3; [ord_tac | Ytac0; Ytac0].
case : (p_or_not_p (x <=o y)) => h2; [ord_tac | Ytac0].
case: (ord_le_to_el oy oz) => h3; first by Ytac0.
case : (p_or_not_p (y <=o z)) => h4; [ord_tac | Ytac0; Ytac0].
move: (ord_le_ltT (proj1 h3) h1) => h6.
by case : (p_or_not_p (x <=o z)) => h5; [ ord_tac| Ytac0].
Qed.

Lemma omax_p1 x y: ordinalp x -> ordinalp y ->
   x <=o (omax x y) /\ y <=o (omax x y).
Proof.
move => ox oy.
rewrite /omax.
move: (ord_leR oy) => yy.
move: (ord_leR ox) => xx.
case: (ord_le_to_ell ox oy).
+ by move => ->; Ytac0.
+ by move => xy; move: (proj1 xy) => h1; Ytac0.
+ move => xy; move: (proj1 xy) => h1.
  by case : (p_or_not_p (x <=o y)) => h2; [ord_tac | Ytac0].
Qed.

Lemma omax_p2 y (c:= cardinal (omax y omega0)):
    ordinalp y -> (infinite_c c /\ inc y (succ_c c)).
Proof.
move:OS_omega => oo oy; move:(omax_p1 oy oo) => [pa pb]; split.
   apply /infinite_c_P2.
   move: (ordinal_cardinal_le1 pb).
   by rewrite cardinal_Bnat.
apply /succ_cP; first by rewrite /c; fprops.
by split=> //; apply: ordinal_cardinal_le1.
Qed.

Lemma omax_p3 x y (c:= cardinal (omax (omax x y) omega0)):
   ordinalp x -> ordinalp y ->
   [/\ infinite_c c, inc x (succ_c c) & inc y (succ_c c)].
Proof.
move => ox oy.
move:(omax_p2 (OS_omax ox oy)); rewrite -/c; move => [ca cb].
move: (omax_p1 ox oy) => [ta tb].
have aux: forall t, t <=o omax x y -> inc t (succ_c c).
   move: (proj1 (CS_succ_c (proj1 ca))) => oc.
   have od: (omax x y) <o (succ_c c) by apply /(ord_ltP oc).
   move => t tc; apply /(ord_ltP oc); ord_tac.
by split => //; apply: aux.
Qed.

Lemma normal_ofs_restriction f C (E := succ_c C):
  infinite_c C-> normal_ofs f ->
  (forall x, inc x E -> inc (f x) E) ->
  normal_function (Lf f E E) E E.
Proof.
move => ice [nfa nfb] Esf.
have ff: function (Lf f E E) by apply: lf_function.
have fp: function_prop (Lf f E E) E E by split; aw.
have si: sincr_ofn (Lf f E E) E by move => a b aE bE /nfa; aw.
split => // a ae /nfb la; aw; rewrite la; congr union.
have asE: sub a E.
   have oe: ordinalp E by exact : (proj1 (CS_succ_c (proj1 ice))).
   move => t ta; exact:(ordinal_transitive oe ae ta).
have asf: sub a (source (Lf f E E)) by aw.
set_extens t.
  by move/funI_P => [z za ->]; apply /(Vf_image_P ff asf);ex_tac; aw;apply: asE.
move/(Vf_image_P ff asf) => [u ua]; move:(asE _ ua) => uE; aw => ->.
apply /funI_P; ex_tac.
Qed.

Definition card_max x y:= cardinal (omax (omax x y) omega0).

Lemma ofs_add_restr a y (c:= card_max a y) (E := succ_c c)
  (f:= Lf (fun z => a +o z) E E) :
  ordinalp a -> ordinalp y ->
  [/\ (forall x, inc x E -> inc (a +o x) E ),
      (forall x, x <=o y -> inc x E),
      normal_function f E E &
      forall x, inc x E -> Vf f x = a +o x].
Proof.
move => oa oy.
move: (omax_p3 oa oy); rewrite -/(card_max _ _) -/c -/E.
move => [icc ae ye].
have pa: forall x, x <=o y -> inc x E.
   move: (proj1 (CS_succ_c (proj1 icc))) => oc.
   have yc:y <o succ_c c by apply/(ord_ltP oc).
   move => x xe; apply/(ord_ltP oc); ord_tac.
have pb: forall x, inc x E -> inc (a +o x) E.
   by move => x xe;apply: succ_c_sum.
move: (normal_ofs_restriction icc (osum_normal oa) pb) => pc.
split => //x xe; rewrite /f; aw.
Qed.

Lemma ofs_mul_restr a y (c:= card_max a y) (E := succ_c c)
  (f:= Lf (fun z => a *o z) E E) :
  \0o <o a -> ordinalp y ->
  [/\ (forall x, inc x E -> inc (a *o x) E ),
      (forall x, x <=o y -> inc x E),
      normal_function f E E &
      forall x, inc x E -> Vf f x = a *o x].
Proof.
move => ap oy.
have oa: ordinalp a by ord_tac.
move: (omax_p3 oa oy); rewrite -/(card_max _ _) -/c -/E.
move => [icc ae ye].
have pa: forall x, x <=o y -> inc x E.
   move: (proj1 (CS_succ_c (proj1 icc))) => oc.
   have yc:y <o succ_c c by apply/(ord_ltP oc).
   move => x xe; apply/(ord_ltP oc); ord_tac.
have pb: forall x, inc x E -> inc (a *o x) E.
   by move => x xe;apply: succ_c_prod.
move: (normal_ofs_restriction icc (oprod_normal ap) pb) => pc.
split => //x xe; rewrite /f; aw.
Qed.

Definition iclosed_set E :=
   (ordinal_set E) /\
   (forall F, sub F E -> nonempty F -> (\osup F = \osup E \/ inc (\osup F) E)).
Definition iclosed_collection (E:property) :=
   ordinal_prop E /\
   (forall F, (forall x, inc x F -> E x) -> nonempty F -> E (\osup F)).

Lemma iclosed_ord x: ordinalp x -> iclosed_set x.
Proof.
move => ox.
have osx: ordinal_set x by move => t tb; ord_tac.
split => // F fo _.
move: (ord_ub_sup1 ox fo) => h.
case: (equal_or_not (union F) x) => e1; last by right; apply /(ord_ltP ox).
left; apply: (ord_sup_1cofinal _ osx); split => // a ax.
have au: a <o union F by rewrite e1; apply /ord_ltP.
have osf: ordinal_set F by move => t /fo tb; ord_tac.
move:(@ord_lt_sup F a osf au)=> [z za [zb _]]; ex_tac.
Qed.

Lemma iclosed_lim: iclosed_collection limit_ordinal.
Proof.
split; first by move => x [].
move => F fl nef.
have os: ordinal_set F by move => x /fl [].
case: (ord_sup_inVlimit os nef); [ by move /fl | done].
Qed.

Lemma iclosed_nonlim:
   ~(iclosed_collection (fun z => ordinalp z /\ ~limit_ordinal z)).
Proof.
move: omega_limit => pa; move: (pa) => [pb _ _].
move /(limit_ordinal_P1 pb): (pa) => [pc pd].
have pe: (forall x, inc x omega0 -> ordinalp x /\ ~ limit_ordinal x).
  move => x /(ord_ltP pb) xo; split; [| move => /omega_limit2 xx];ord_tac.
by move => [_ h]; move: (h _ pe pc); rewrite -pd; move=> [_].
Qed.

Lemma iclosed_fixpoints f (P:= fun z => ordinalp z /\ f z = z):
    normal_ofs f ->
    (iclosed_collection P) /\ non_coll P.
Proof.
move => nf; split; last first.
  apply:unbounded_non_coll; first by move => x [].
  move => x ox.
  move: (normal_ofs_fix nf ox) => [pa pb _].
  exists (the_least_fixedpoint_ge f x) => //; split => //; ord_tac.
split; [by move => t [] | move => F fp nef ].
move /normal_ofs_equiv1: (nf) => [pa pb].
have pc: (forall x, inc x F -> \0o <=o x) by move =>x /fp [ox _]; ord_tac1.
have pd: (fun_image F f) = F.
  set_extens t.
     by move => /funI_P [z zf ->]; rewrite (proj2 (fp _ zf)).
  by move => tf; apply /funI_P; ex_tac; rewrite (proj2 (fp _ tf)).
move: (pb _ pc nef); rewrite pd => h; split => //; apply: OS_sup.
move => t /pc ta;ord_tac.
Qed.

Lemma iclosed_fixpoints_fun f a :
  ordinalp a -> normal_function f a a -> iclosed_set (fixpoints f).
Proof.
move => oa na; move:(na) => [[ff sf tf] pb pc].
rewrite /fixpoints sf;split; first by move => t /Zo_S h; ord_tac0.
set E := Zo a _;move => F fp nef.
have subfa: sub F a by move => t /fp /Zo_S.
have ose: ordinal_set E by move =>t /Zo_S h; ord_tac.
move: (ord_sup_M fp ose) => l1.
have h: \osup E <=o a by apply:ord_ub_sup1 => //; apply : Zo_S.
case: (equal_or_not (\osup F) a) => sna.
  rewrite - sna in h; left; ord_tac.
case: (normal_function_equiv oa oa na subfa nef) => //.
have ->: (image_by_fun f F) = F.
  have aux: sub F (source f) by ue.
   set_extens t.
     by move => /(Vf_image_P ff aux) [z zf ->]; rewrite (Zo_hi (fp _ zf)).
   by move => zf; apply /(Vf_image_P ff aux); ex_tac; rewrite (Zo_hi (fp _ zf)).
move => fxp;right; apply: Zo_i => //.
apply /(ord_ltP oa); split => //;ord_tac.
Qed.

Lemma iclosed_normal_fun f x y:
  ordinalp x -> ordinalp y -> normal_function f x y ->
  iclosed_set (range (graph f)).
Proof.
move => ox oy nf; move: (nf)=> [[ff sf tf] pb pc]; split.
  move =>t /(f_range_graph ff); rewrite tf => h; ord_tac.
move => F fr [w wf].
set G := Zo (source f) (fun z => inc (Vf f z) F).
have sgx: sub G x by rewrite - sf; apply:Zo_S.
have neG: nonempty G.
  move /(range_fP ff): (fr _ wf) => [u uf uv]; exists u; apply:Zo_i => //; ue.
move: (ord_ub_sup1 ox sgx) => le1.
have sG: sub G (source f) by ue.
case: (equal_or_not (\osup G) x) => sx.
  have og: ordinal_set G by move => t /Zo_S; rewrite sf => ta; ord_tac.
  rewrite - sf in pb.
  left; apply: ord_sup_1cofinal; first split => //; last first.
    move =>t /(f_range_graph ff); rewrite tf => h; ord_tac.
  move => b /(range_fP ff) [u usf ->].
  have ua': u <o \osup G by rewrite sx; apply /(ord_ltP ox); ue.
  move: (ord_lt_sup og ua') => [v vg uv].
  move /Zo_hi: (vg) => vf;ex_tac; exact (proj1 (pb _ _ usf (Zo_S vg) uv)).
have <-: image_by_fun f G = F.
  set_extens t; first by move /(Vf_image_P ff sG)=> [u /Zo_hi h ->].
  move => tF; apply /(Vf_image_P ff sG).
  move /(range_fP ff): (fr _ tF)=> [u usf uv]; exists u => //.
  apply: Zo_i => //; ue.
case: (normal_function_equiv ox oy nf sgx neG) => // <-; right.
apply /(range_fP ff); exists (\osup G) => //; rewrite sf.
by apply/(ord_ltP ox).
Qed.

Lemma iclosed_normal_ofs1 f u (P := fun z => exists2 x, u <=o x & z = f x):
  ordinalp u -> normal_ofs1 f u ->
  (iclosed_collection P /\ non_coll P).
Proof.
move => ou [na nb].
move: (ofs_sincru na) => ha.
move: (osum_increasing5 ou na) =>[_ [b ub h]].
have oP: ordinal_prop P by move => x [y /ha uy ->].
split; last first.
  apply:unbounded_non_coll => // x ox.
  case: (ord_le_to_ee (proj32 ub) ox) => bx.
     exists (f x); [ by apply:h | exists x => //; ord_tac].
  exists (f b); [move: (h _ (ord_leR (proj32 ub))) => h1; ord_tac |by exists b].
split => //.
move => F Fi nef.
pose p z t:= u <=o t /\ z = f t.
pose g x := choose (p x).
set E:= fun_image F g.
have Cp: forall a z, u <=o a -> z = f a -> u <=o (g z) /\ z = f (g z).
  by move => a z ua zf; apply: (choose_pr (p:=p z)); exists a.
have CP1:forall a, u <=o a -> a = g (f a).
  move => a au; move: (Cp _ _ au (erefl (f a))) => [pa pb].
  case: (ord_le_to_ell (proj32 au) (proj32 pa)) => // hb.
      by move: (proj2 (na _ _ au hb)); rewrite {1} pb.
 by move: (proj2 (na _ _ pa hb)); rewrite - pb.
have Fv: F = fun_image E f.
  set_extens w.
    move => wF; apply/funI_P; move: (Fi _ wF) => [t ta tb]; exists t => //.
    by apply /funI_P; exists w => //; rewrite tb; apply: CP1.
  move /funI_P => [x xE ->].
  move /funI_P: (xE) => [z zf xf]; move:(Fi _ zf) => [t ta tb].
  by move: (CP1 _ ta); rewrite - tb - xf => <-; rewrite - tb.
have pa: forall x, inc x E -> u <=o x /\ g (f x) = x.
  move => w /funI_P [z zf zv]; move: (Fi _ zf) => [t ta tb].
  have tc: exists t, u <=o t /\ z = f t by exists t.
  move: (choose_pr tc); rewrite -/(g _) - zv; move => [la <-]; split => //.
have Ea: (forall x, inc x E -> u <=o x) by move => x /pa [].
move: nef => [t0 t0f].
have fit0: inc (g t0) E by apply/funI_P; ex_tac.
have ne: nonempty E by ex_tac.
have: u <=o \osup E.
  apply: (ord_leT (Ea _ fit0)); apply: ord_sup_ub => // t /Ea ut; ord_tac.
by move: (nb _ Ea ne); rewrite -Fv => ->; exists (union E).
Qed.

Lemma iclosed_normal_ofs f (P := fun z => exists2 x, ordinalp x & z = f x):
  normal_ofs f ->
  (iclosed_collection P /\ non_coll P).
Proof.
move => h.
have sb: normal_ofs1 f \0o by apply/normal_ofs_equiv1.
move: (iclosed_normal_ofs1 OS0 sb)=> [[pa pb] pc].
have aux: forall z, P z <-> exists2 x, \0o <=o x & z = f x.
  move => z; split; move => [x xp ->]; exists x => //; [ord_tac1 |ord_tac].
split => //; first split.
+ by move => t [x ox ->]; apply(ofs_sincr (proj1 h)).
+ by move => g pF nef; apply /aux; apply: pb => // x/pF => w; apply/aux.
+ by move => [E ev]; case:pc; exists E => x; split; [move/ev/aux| move/aux/ev].
Qed.

Lemma normal_fix_points_similara f C (E:= succ_c C): infinite_c C ->
  normal_ofs f ->
  (forall x, inc x E -> inc (f x) E) ->
  (ord_cofinal (Zo E (fun z => f z = z)) E).
Proof.
move => icE nf fee.
split => //; first by apply: Zo_S.
move => x xE.
move: (next_fix_point_small icE nf fee xE).
move/(succ_cP (proj1 icE)): (xE) => [ox ob].
move: (normal_ofs_fix nf ox) => []; set y := the_least_fixedpoint_ge f x.
by move => qa qb _ qc; exists y => //; apply:Zo_i.
Qed.

Lemma normal_fix_points_similarb f C (E:= succ_c C): infinite_c C ->
  normal_ofs f ->
  (forall x, inc x E -> inc (f x) E) ->
  cardinal (Zo E (fun z => f z = z)) = E.
Proof.
move => icE nf fee; apply:ord_cofinal_p4 => //.
exact: (normal_fix_points_similara icE nf fee).
Qed.