Library sset12

Theory of Sets : Ordinals

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

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

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

Module Ordinals2.

Normal ordinal functional symbols


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.

Indexing a collection of ordinals


Definition collectivising_srel (r: relation) :=
   forall x, r x x -> exists E, (forall y, inc y E <-> r y x).
Definition worder_rc r := worder_r r /\ collectivising_srel r.

Definition segmentr (r: relation) x :=
   choose (fun E => (forall y, inc y E <-> (r y x /\ y <> x))).

Definition ordinalr r x := ordinal (graph_on r (segmentr r x)).

Lemma segmentrP r x: collectivising_srel r -> r x x ->
   (forall y, (inc y (segmentr r x) <-> r y x /\ y <> x)).
Proof.
move => pa pb; move: (pa _ pb) => [E Ep].
pose p E:= forall y, inc y E <-> r y x /\ y <> x.
rewrite -/(p _); apply: (choose_pr); exists (E -s1 x) => y; split.
  by move/setC1_P => [/Ep sa sb].
by move => [/Ep sa sb]; apply /setC1_P.
Qed.

Lemma worder_rc_seg (r: relation) x:
  worder_rc r -> r x x ->
  worder_on (graph_on r (segmentr r x)) (segmentr r x).
Proof.
move => [pa pb] rxx; apply: (wordering_pr pa).
move => a /(segmentrP pb rxx) [pc _].
by move: (pa) => [[_ _ rr] _]; move: (rr _ _ pc) => [].
Qed.

Lemma OS_ordinalr r x:
  worder_rc r -> r x x -> ordinalp (ordinalr r x).
Proof. by move => pa /(worder_rc_seg pa) [pc _]; apply: OS_ordinal. Qed.

Lemma ordinalr_Mle r x y: worder_rc r -> r x y ->
   (ordinalr r x) <=o (ordinalr r y).
Proof.
move => pa px.
move: (proj33 (proj1 (proj1 pa)) _ _ px) => [rxx ryy].
move: (proj1 (worder_rc_seg pa rxx)) (proj1 (worder_rc_seg pa ryy)) => ha hb.
apply: order_cp2 => //.
have ss: sub (segmentr r x) (segmentr r y).
  move => t /(segmentrP (proj2 pa) rxx)[sa sb].
  move: (proj31 (proj1 (proj1 pa)) _ _ _ sa px) => ty.
  apply/(segmentrP (proj2 pa) ryy); split => //.
  move => ety; rewrite - ety in px.
  by move: (proj32_1 (proj1 pa) _ _ sa px).
apply/(order_cp0 (proj1 ha) (proj1 hb)) => u v.
by move /graph_on_P1 => [sa sb sc]; apply /graph_on_P1; split => //; apply: ss.
Qed.

Lemma ordinalr_Mlt r x y: worder_rc r -> r x y -> x <> y ->
   (ordinalr r x) <o (ordinalr r y).
Proof.
move => pa px xny.
move: (pa) => [[[rt ra rr] _] csr].
have [rxx ryy] := (rr _ _ px).
move: (segmentrP csr rxx) (segmentrP csr ryy) => sx sy.
have ss: sub (segmentr r x) (segmentr r y).
  move => t /sx [sa sb].
  move: (rt _ _ _ sa px) => ty; apply/sy; split => //.
  move => ety; rewrite - ety in px.
  by move: (ra _ _ sa px).
move: (proj1 (worder_rc_seg pa rxx)) (proj1 (worder_rc_seg pa ryy)) => ha hb.
have pb: sub (graph_on r (segmentr r x)) (graph_on r (segmentr r y)).
  apply/(order_cp0 (proj1 ha) (proj1 hb)) => u v.
  by move/graph_on_P1 => [sa sb sc]; apply /graph_on_P1; split => //; apply: ss.
have pc: forall z, r z z ->
   substrate (graph_on r (segmentr r z)) = (segmentr r z).
  move => z rzz; apply :graph_on_sr => a /(segmentrP csr rzz) [xx _].
  by move: (rr _ _ xx) => [].
have xsy: inc x (segmentr r y) by apply /sy.
apply: order_cp3 => //.
  split => // eq; move: (f_equal substrate eq).
  rewrite (pc _ rxx) (pc _ ryy) => h.
  by move: xsy; rewrite -h; move/sx =>[_].
rewrite (pc _ rxx); red; rewrite (pc _ ryy); split => //.
move => a b /sx [sa sb] /graph_on_P1 [h1 h2 h3]; apply /sx.
move: (rt _ _ _ h3 sa) => bx; split => // ebx.
by rewrite ebx in h3; move: (ra _ _ sa h3).
Qed.

Lemma ordinalr_segment r a x (b:=ordinalr r x):
   worder_rc r -> r x x -> a <=o b ->
   (exists2 y, r y y & a = ordinalr r y).
Proof.
move => woc rxx ab.
case: (equal_or_not a b); [by move ->; exists x | move => nab].
have iab: inc a b by apply /ord_ltP; [ord_tac | split ].
move: (worder_rc_seg woc rxx) => [pa pb].
move: (the_ordinal_iso1 pa) => [].
rewrite -/(ordinalr _ _) pb ordinal_o_sr.
set gr := (graph_on r (segmentr r x)); set f := (the_ordinal_iso gr).
set oor := (ordinal_o (ordinalr r x)).
move => sa sb [[[ff injf] [_ sjf]] sf tf] sd.
have asf: inc a (source f) by ue.
move: (Vf_target ff asf); rewrite tf.
set y := Vf f a; set rs:= (graph_on r (segmentr r y)).
move /(segmentrP (proj2 woc) rxx) => [ryx xny].
move: (proj1 (proj1 woc)) => or.
move: (proj33 or _ _ ryx) => [ryy _].
move:(segmentrP (proj2 woc) ryy) => sP.
set g:= Lf (Vf f) a (segmentr r y).
move: (ab) => [oa ob sab].
suff oih:order_isomorphism g (ordinal_o a) rs.
  have h : ordinal_o a \Is rs by exists g.
  move: (worder_invariance h (ordinal_o_wor oa)) => tt.
  by exists y => //; rewrite - (ordinal_o_isu2 tt oa (orderIS h)).
have srr: substrate rs = (segmentr r y).
   by apply:graph_on_sr => u /sP [/(proj33 or) []].
have saf: sub a (source f) by ue.
have la: lf_axiom (Vf f) a (segmentr r y).
  move => s ssa; apply /sP; rewrite /y; move: (saf _ ssa) => isf.
  split; last first.
    move/(injf _ _ isf asf) => esa.
    by case: (ordinal_irreflexive oa); rewrite -{1} esa.
  have:gle oor s a.
    apply /graph_on_P1;rewrite - sf; split => //.
    exact: (ordinal_transitive oa ssa).
  by move /(sd s a isf asf) => /graph_on_P1 [].
hnf; rewrite (ordinal_o_sr) srr.
split => //; [ fprops | apply: (order_from_rel _ or) | |].
  red; rewrite /g; aw; split => //; apply: lf_bijective => //.
    by move => u v ua va; apply injf; apply: saf.
  move => c /sP [c1 c2].
  have: inc c (target f).
     rewrite tf; apply /(segmentrP (proj2 woc) rxx).
     move: (proj31 or _ _ _ c1 ryx)=> cx; split => //.
     by move => ecx; rewrite -ecx in ryx;move: (proj32 or _ _ c1 ryx).
  move /sjf => [d dsf dv]; exists d; last by rewrite dv.
  have od: ordinalp d by rewrite sf in dsf; exact: (ordinal_hi ob dsf).
  case:(ord_le_to_si oa od) => // sad.
  have: gle oor a d by apply /sub_gleP; split => //; ue.
  move /(sd _ _ asf dsf) => /graph_on_P1 [_ _];rewrite dv -/y => yc.
  case: c2; exact (proj32 or _ _ c1 yc).
hnf; rewrite /g;aw => u v ua va; aw.
move: (saf _ ua) (saf _ va) =>ub vb.
move: (sd u v ub vb) => h;split.
  move/sub_gleP=> [_ _ h1]; apply/graph_on_P1; split; try apply: la => //.
  suff:gle gr (Vf f u) (Vf f v) by move/graph_on_P1 =>[].
  by apply /h; apply/sub_gleP; rewrite - sf.
move/graph_on_P1 => [_ _ h1]; apply/sub_gleP; split => //.
suff:gle gr (Vf f u) (Vf f v) by move/h /sub_gleP=> [].
apply/graph_on_P1; split => //; Wtac.
Qed.

Definition ordinals r a := choose (fun x => r x x /\ a = ordinalr r x).

Lemma ordinalsP r a: worder_rc r ->
  (exists2 x, r x x & a = ordinalr r x) ->
  (r (ordinals r a) (ordinals r a) /\ ordinalr r (ordinals r a) = a).
Proof.
move => pa [x rxx av].
pose p x := (r x x /\ a = ordinalr r x).
rewrite /ordinals -/p.
have exp : exists x, p x by exists x.
by move: (choose_pr exp); set q := (choose p); move => [rqq ->].
Qed.

Lemma ordinalsrP r x: worder_rc r -> r x x ->
  ordinals r (ordinalr r x) = x.
Proof.
move => pa pb.
set a := (ordinalr r x).
have: (exists2 x, r x x & a = ordinalr r x) by exists x.
move /(ordinalsP pa); set q := ordinals r a; move => [rqq qv].
ex_middle bad.
case: (worderr_total (proj1 pa) rqq pb) => h.
  by move: (ordinalr_Mlt pa h bad) => [_]; rewrite qv.
by move: (ordinalr_Mlt pa h (nesym bad))=> [_]; rewrite qv.
Qed.

Lemma ordinals_non_coll1 r: worder_rc r ->
   (non_coll (fun x => r x x)) ->
   (forall a, ordinalp a -> exists2 x, r x x & a = ordinalr r x).
Proof.
move => pa pb a oa; ex_middle npa; case: pb.
exists (Zo (fun_image a (ordinals r)) (fun z => r z z)).
move => x; split; first by move /Zo_hi.
move => rxx; apply /Zo_P; split => //; apply /funI_P.
have osx:= (OS_ordinalr pa rxx).
have eq:= (ordinalsrP pa rxx).
have: ordinalr r x <o a.
  by case: (ord_le_to_el oa osx) => // alx; move:(ordinalr_segment pa rxx alx).
move /ord_ltP0 => [_ _ za]; ex_tac.
Qed.

Lemma ordinals_Mle r a b: worder_rc r ->
   (non_coll (fun x => r x x)) ->
   a <=o b -> r (ordinals r a) (ordinals r b).
Proof.
move => ha hb ab.
move: (ordinalsP ha (ordinals_non_coll1 ha hb (proj31 ab))).
move: (ordinalsP ha (ordinals_non_coll1 ha hb (proj32 ab))).
set sa := (ordinals r a); set sb := (ordinals r b).
move => [rbb vb][raa va].
case: (worderr_total (proj1 ha) raa rbb) => // h.
move:(ordinalr_Mle ha h); rewrite va vb => ba.
by move: raa; rewrite /sa /sb (ord_leA ab ba).
Qed.

Lemma ordinals_Mlt r a b: worder_rc r ->
   (non_coll (fun x => r x x)) ->
   a <o b ->
  (r (ordinals r a) (ordinals r b) /\ (ordinals r a) <> (ordinals r b)).
Proof.
move => pa pb [pc pd]; move:(ordinals_Mle pa pb pc) => h.
split => // sv.
move: (pc) => [oa ob _].
have sa: (exists2 x, r x x & a = ordinalr r x) by apply:ordinals_non_coll1.
have sb: (exists2 x, r x x & b = ordinalr r x) by apply:ordinals_non_coll1.
by case: pd; rewrite - (proj2 (ordinalsP pa sa)) - (proj2 (ordinalsP pa sb)) sv.
Qed.

Lemma collectivising_srel_ord (r:relation):
  (forall x y, r x y -> x <=o y) -> collectivising_srel r.
Proof.
move => h1 x /h1 xx.
have ox: ordinalp x by ord_tac.
exists (Zo (succ_o x) (r^~ x)); move => y;split; first by move /Zo_hi.
by move => ryx; apply:Zo_i => //; apply /(ord_leP ox); apply: h1.
Qed.

Lemma collectivising_srel_ord_seg (r:relation) :
  (forall x y, r x y -> x <=o y) ->
  forall x, r x x -> segmentr r x = Zo x (fun z => r z x).
Proof.
move => ro x rxx.
move: (proj31 (ro _ _ rxx)) => ox.
move:(collectivising_srel_ord ro) => cr.
set_extens t.
  move /(segmentrP cr rxx) => [pa pb]; apply:Zo_i => //.
  by apply/(ord_ltP ox); split => //; apply: ro.
move => /Zo_P[pa pb]; apply /(segmentrP cr rxx); split => //.
by move=> tx; case: (ordinal_decent ox pa); rewrite {2} tx.
Qed.

Lemma worder_rc_ord (r:relation) :
  (forall x y, r x y -> x <=o y) ->
  (order_r r) -> (forall x y, r x x -> r y y -> (r x y \/ r y x)) ->
  worder_rc r.
Proof.
move=> h1 h2 h3; split.
  split => // x hx [w wx].
  move: (proj31 (h1 _ _ (hx _ wx))) => ow.
  move: (least_ordinal4 ow wx (p:=inc^~x)); set y := least_ordinal _ _.
  move=> [oy yx yl]; rewrite /least (graph_on_sr hx); exists y; split => //.
  move => t tx; apply /graph_on_P1; split => //.
  case: (h3 _ _ (hx _ yx) (hx _ tx)) => // /h1 ty.
  move: (proj31 (h1 _ _ (hx _ tx))) => ot.
  by move: (yl _ ot tx) => yt; rewrite (ord_leA ty yt); apply: hx.
move => x /h1 xx.
have ox: ordinalp x by ord_tac.
exists (Zo (succ_o x) (r^~ x)); move => y;split; first by move /Zo_hi.
by move => ryx; apply:Zo_i => //; apply /(ord_leP ox); apply: h1.
Qed.

Lemma worder_rc_op (p:property) :
  worder_rc (fun x y => [/\ p x, p y & x <=o y]).
Proof.
apply: worder_rc_ord.
- by move => x y [_ _].
- split.
  + move =>x y z [pa pb pc][pd pe pf]; split => //; ord_tac.
  + move =>x y [_ _ pc][ _ _ pf] ; ord_tac.
  + move => x y [pa pb pc]; split; split => //; apply: ord_leR; ord_tac.
- move => x y [pa _ [pc _ _]][ pb _ [pf _ _]].
  by case: (ord_le_to_ee pc pf) => le; [left | right]; split.
Qed.

Lemma ordinalrsP (p: property) (r := fun x y => [/\ p x, p y & x <=o y])
   x (y := ordinalr r x):
   ordinal_prop p -> p x -> (ordinalp y) /\ ordinals r y = x.
Proof.
move => op px; move:(op _ px) => ox.
move: (worder_rc_op p) => pa.
have rxx: r x x by split => //; ord_tac.
move:(ordinalsrP pa rxx) => h; split => //; by apply: OS_ordinalr.
Qed.

Lemma ordinals_set_iso E (p := inc ^~E)
      (r:= fun x y => [/\ p x, p y & x <=o y])
      (A:= ordinal (graph_on ordinal_le E)):
  (ordinal_set E) ->
  (lf_axiom (ordinals r) A E) /\
  order_isomorphism (Lf (ordinals r) A E) (ordinal_o A) (graph_on ordinal_le E).
Proof.
move => pa.
move: (worder_rc_op p) ; rewrite -/r => pc.
have ose: (forall a, inc a E -> a <=o a) by move => a /pa op; ord_tac.
have rxx: forall x, r x x <-> inc x E.
  move => x; split; [ by move =>[] | move => xE;split; fprops ].
pose H a := (exists2 x, r x x & a = ordinalr r x).
have pd: forall a, H a ->
    (r (ordinals r a) (ordinals r a) /\ ordinalr r (ordinals r a) = a).
  by move => a ha; apply: ordinalsP.
have pe: forall x, inc x E -> ordinals r (ordinalr r x) = x.
  by move => x /rxx xe;apply: ordinalsrP.
move: (wordering_ordinal_le_pr pa) => [sc sd].
have ra: forall x, inc x E -> inc (ordinalr r x) A.
  move => x /rxx xE; suff: (ordinalr r x) <o A by move /ord_ltP0 => [].
  move: (worder_rc_seg pc xE) => []; rewrite -/r => [sa sb].
  move: (segmentrP (proj2 pc) xE); rewrite -/r => sp.
  apply: order_cp3 => //; first split.
       apply /(order_cp0 (proj1 sa) (proj1 sc))=> u v.
       by move/graph_on_P1 => [_ _ uv];apply/graph_on_P1.
    move => h;move:(f_equal substrate h); rewrite sb sd => ss.
    by move /rxx:(xE); rewrite - ss; move /sp => [_].
  red; rewrite sb sd;split; first by move =>t /sp [] [].
  move => u v /sp [[pu px ux] nux] /graph_on_P1 [ve _ vu]; apply /sp; split.
    split => //; ord_tac.
    move => vx; case: nux; rewrite vx in vu; ord_tac.
have rb:forall a, inc a A -> H a.
  move => a aA.
  move: (the_ordinal_iso1 sc); rewrite -/A; set f:= the_ordinal_iso _.
  rewrite /order_isomorphism sd ordinal_o_sr.
  move => [sa sb [[[ff injf] [_ sjf]] sf tf] isf].
  red in isf; rewrite sf in injf isf.
  set x := Vf f a.
  have xe: r x x by apply /rxx;rewrite - tf /x; Wtac.
  move:(worder_rc_seg pc xe)=> [ta tb].
  have oA:ordinalp A by exact: (OS_ordinal sc).
  have oa :=(ordinal_hi oA aA).
  have saA :=(ordinal_transitive oA aA).
  exists x => //; symmetry;rewrite /ordinalr;apply: ordinal_o_isu2 => //.
  have la: lf_axiom (Vf f) a (segmentr r x).
    move => t ita; move: (saA _ ita) => tA.
    have [[_ _ lte] nta]: t <o a by apply /ord_ltP.
    have: gle (ordinal_o A) t a by apply /sub_gleP.
    move /(isf _ _ tA aA) => /graph_on_P1.
    move => h; apply /(segmentrP (proj2 pc) xe); split => //.
    by move => hh; case: nta; apply/ (injf _ _ tA aA).
  apply:orderIS;exists (Lf (Vf f) a (segmentr r x)).
  red; rewrite tb ordinal_o_sr; split; fprops.
    red; aw; split => //; apply: lf_bijective => //.
      move => u v /saA ua /saA va; apply /(injf _ _ ua va).
    move => y /(segmentrP (proj2 pc) xe) [[yE _ rxy] xny].
    rewrite tf in sjf;move: (sjf _ yE) => [];rewrite sf => [b bA bb].
    case: (ord_le_to_el (ordinal_hi oA aA) (ordinal_hi oA bA)).
      move => [_ _ ab]; have: gle (ordinal_o A) a b by apply /sub_gleP.
      move /(isf _ _ aA bA) => /graph_on_P1 [_ _];rewrite bb - /x => xy.
      case: xny; ord_tac.
    move /(ord_ltP oa) => ba; ex_tac.
  red; aw;move => u v ua va; aw; move: (saA _ ua) (saA _ va) => uA vA; split.
    move/sub_gleP=> [_ _ h1]; have: gle (ordinal_o A) u v by apply /sub_gleP.
    move /(isf _ _ uA vA) => /graph_on_P1 [_ _ le].
    apply/graph_on_P1; split;try apply: la => //; split => //; red; Wtac.
  move /graph_on_P1 => [_ _ [_ _ le]].
  have:(gle (graph_on ordinal_le E) (Vf f u) (Vf f v)).
    apply/graph_on_P1; split => //; Wtac.
  by move /(isf _ _ uA vA) => /sub_gleP [_ _ h1]; apply/sub_gleP.
set fp := ordinals r.
have rc: forall a, inc a A -> inc (fp a) E /\ ordinalr r (fp a) = a.
  by move => a /rb /pd [/rxx sa sb].
set f := Lf fp A E.
have lfa: lf_axiom fp A E by move => t /rc [].
have bf: bijection_prop f A E.
  red;rewrite /f; aw; split => //; apply: lf_bijective.
  - by exact.
  - by move => u v /rc [_ e1] /rc [_ e2] e3; rewrite - e1 - e2 e3.
  - by move => y yE; rewrite -(pe _ yE); move: (ra _ yE) => h; ex_tac.
split => //.
split => //; [ apply: ordinal_o_or | fprops | by rewrite ordinal_o_sr sd |].
hnf; rewrite /f; aw; move => x y xA yA; aw.
move: (rc _ xA) (rc _ yA) => [ta tb][tc td]; split => h.
  move:(proj2 (worder_total sc));rewrite sd => to;case: (to _ _ ta tc) => //hh.
  move /sub_gleP:h => [_ _ ce].
  suff: x = y by move => h1; move: hh; rewrite h1.
  move/graph_on_P1:hh => /(ordinalr_Mle pc).
  by rewrite tb td; move => [_ _ cp]; apply: extensionality.
move/graph_on_P1:h => /(ordinalr_Mle pc).
by rewrite tb td; move => [_ _ cp];apply/sub_gleP.
Qed.

Lemma ordinals_set_normal E (p := inc ^~E)
      (r:= fun x y => [/\ p x, p y & x <=o y])
      (A:= ordinal (graph_on ordinal_le E))
      (f:= Lf (ordinals r) A E):
  (iclosed_set E) ->
  normal_function f A E.
Proof.
move => [pa pb].
move: (proj2 (ordinals_set_iso pa)); rewrite -/f -/A.
move => [o1 o2 [[[ff injf] [_ sjf]] sf tf] fincr].
move: (worder_rc_op p) ; rewrite -/r => pc.
move: (wordering_ordinal_le_pr pa) => [sc sd].
rewrite sd in tf; rewrite ordinal_o_sr in sf.
have fi: forall a b, inc a A -> inc b A -> a <o b -> Vf f a <o Vf f b.
   red in fincr; rewrite sf in fincr injf.
   move => a b asf bsf [lab nab]; split.
     have: gle (ordinal_o A) a b by move: lab => [_ _ lab]; apply/sub_gleP.
     by move /(fincr _ _ asf bsf) => /graph_on_P1 [].
   by move => h; move: (injf _ _ asf bsf h).
split => // a aA la.
have oA:ordinalp A by exact: (OS_ordinal sc).
set F :=(image_by_fun f a).
have asf: sub a (source f) by rewrite sf; apply: (ordinal_transitive oA).
have sfe: sub F E by rewrite -tf ; apply:fun_image_Starget1.
have nef: nonempty F.
   exists (Vf f \0o); apply /(Vf_image_P ff asf); exists \0o => //.
   exact (proj32 la).
have osF: ordinal_set F by move => t /sfe; apply: pa.
have faE: inc (Vf f a) E by rewrite -tf; Wtac.
move: (ord_sup_ub pa faE) => suE.
have ofa: ordinalp (Vf f a) by apply: pa.
have bfa : ordinal_ub F (Vf f a).
  move => t /(Vf_image_P ff asf) [u ua ->].
  move: (ordinal_transitive oA aA ua) => uA.
  move /(ord_ltP (proj31 la)): ua => ua.
  exact (proj1 (fi _ _ uA aA ua)).
move: (ord_ub_sup osF ofa bfa) => pr1.
case: (pb _ sfe nef) => H; first by rewrite - H in suE; ord_tac.
rewrite tf in sjf; move: (sjf _ H); rewrite sf; move => [b bA bv].
move: (ordinal_hi oA aA) (ordinal_hi oA bA) => oa ob.
case: (ord_le_to_ell oa ob) => ab; first by ue.
  move: (fi _ _ aA bA ab); rewrite bv => h; ord_tac.
have sb: succ_o b <o a by move /(limit_ordinal_P3): la => [ _]; apply.
have sbb: inc (succ_o b) a by apply /(ord_ltP oa).
have osbA: inc (succ_o b) A by apply: (ordinal_transitive oA aA).
move:(fi _ _ bA osbA (ord_succ_lt ob)) => h.
have: inc (Vf f (succ_o b)) F by apply/(Vf_image_P ff asf); ex_tac.
move /(ord_sup_ub osF); rewrite - bv => h1; ord_tac.
Qed.

Definition ordinalsE E B :=
  Lf (ordinals (fun x y => [/\ inc x B, inc y B & x <=o y])) E E.

Lemma ordinals_set_normal1 C (E:= succ_c C) B (f:= ordinalsE E B):
  infinite_c C -> iclosed_set B -> ord_cofinal B E ->
  [/\ lf_axiom (ordinals (fun x y=> [/\ inc x B, inc y B & x <=o y])) E E ,
    normal_function f E E & image_of_fun f = B].
Proof.
move => pa pb pc.
move: (ord_cofinal_p5 pa pc); rewrite -/E => eq1.
move: (ordinals_set_normal pb) (ordinals_set_iso (proj1 pb)).
rewrite eq1; set g := (Lf (ordinals _) E B); move => [p1 p2 p3] [pd pe].
have sbe: sub B E by move: pc => [].
have pf: lf_axiom (ordinals (fun x y=> [/\ inc x B, inc y B & x <=o y])) E E
   by move => t /pd /sbe.
have ff: function f by apply: lf_function.
have fg: function g by apply: lf_function.
have oe: ordinalp E by move:(succ_c_pr1 (proj1 pa)) => [[]].
have sf: forall x, inc x E -> Vf f x = Vf g x.
   move => x xe; rewrite /f/ordinalsE/g; aw.
have imf: image_of_fun f = B.
   set_extens t.
     move /(Vf_image_P1 ff);rewrite /f/ordinalsE; aw.
     by move=> [u ua ->]; aw; apply: pd.
   move => tb;move: pe => [_ _ [[_ [_ p4]] _ _] _].
   have ttg: inc t (target g) by rewrite /g; aw.
   have sg: source g = E by rewrite /g; aw.
   move: (p4 _ ttg) => [u ua <-]; rewrite - sf; last by ue.
   apply /(Vf_image_P1 ff); exists u => //;rewrite /f/ordinalsE; aw; ue.
split => //; split => //.
+ by rewrite /f /ordinalsE/function_prop;aw.
+ by move => x y xe ye xy; rewrite sf // sf //; apply: p2.
+ move => x xe lx; rewrite sf // (p3 x xe lx).
  have sxe :=(ordinal_transitive oe xe).
  have sa: sub x (source g) by rewrite /g; aw.
  have sb: sub x (source f) by rewrite /f/ordinalsE; aw.
  congr union; set_extens y.
    move /(Vf_image_P fg sa) => [u ux ->]; rewrite - sf //; last by apply: sxe.
    apply /(Vf_image_P ff sb); ex_tac.
  move /(Vf_image_P ff sb) => [u ux ->]; rewrite sf //; last by apply: sxe.
  apply /(Vf_image_P fg sa); ex_tac.
Qed.

Lemma ordinals2_extc C1 C2 B1 B2
    (E1 :=succ_c C1)(E2 :=succ_c C2) :
  infinite_c C1 -> infinite_c C2 ->
  iclosed_set B1 -> iclosed_set B2 ->
  ord_cofinal B1 E1 -> ord_cofinal B2 E2 ->
  C1 <=c C2 -> B1 = B2 \cap E1 ->
  agrees_on E1 (ordinalsE E1 B1) (ordinalsE E2 B2).
Proof.
move => ic1 ic2 cl1 cl2 cf1 cf2 c1c2 iv.
move: (ordinals_set_normal1 ic1 cl1 cf1).
move: (ordinals_set_normal1 ic2 cl2 cf2).
rewrite -/E1 -/E2.
have E1E2: sub E1 E2.
   move => x /(succ_cP (proj1 ic1)) [sa sb]; apply/(succ_cP (proj1 ic2)).
   split => //; co_tac.
set f1 := (ordinalsE E1 B1); set f2 := (ordinalsE E2 B2).
move => [ax2 [[ff2 sf2 tf2] ninc2 cont2] im2].
move => [ax1 [[ff1 sf1 tf1] ninc1 cont1] im1].
have B1B2: sub B1 B2 by rewrite iv; apply: subsetI2l.
have oe2: ordinalp E2 by move:(succ_c_pr1 (proj1 ic2)) => [[]].
have oe1: ordinalp E1 by move:(succ_c_pr1 (proj1 ic1)) => [[]].
have ob2: ordinal_set B2 by move => t /(proj1 cf2) te; ord_tac.
have ob1: ordinal_set B1 by move => t /B1B2 /ob2.
move: (ordinals_set_iso ob1) => [].
rewrite (ord_cofinal_p5 ic1 cf1).
move: (ordinals_set_iso ob2) => [].
rewrite (ord_cofinal_p5 ic2 cf2).
set r1 := (fun x0 y : Set => [/\ inc x0 B1, inc y B1 & x0 <=o y]).
set r2 := (fun x0 y : Set => [/\ inc x0 B2, inc y B2 & x0 <=o y]).
rewrite -/E1 -/E2; move => ua2 ub2 ua1 ub1.
move: (inverse_order_is ub2).
set g2 := (Lf (ordinals r2) E2 B2); set g2' := inverse_fun g2 => ub3.
have sr2: (substrate (graph_on ordinal_le B2)) = B2.
  rewrite graph_on_sr // => a /ob2 or; ord_tac.
have sr1: (substrate (graph_on ordinal_le B1)) = B1.
  rewrite graph_on_sr // => a /ob1 or; ord_tac.
move: (ub3) => [_ _ bf _]; move: bf; rewrite sr2 ordinal_o_sr => bg2.
have sg2: source g2' = B2 by move: bg2 => [_ fb _].
have sa: forall x, inc x E1 -> inc (Vf g2' (ordinals r1 x)) E2.
  move => x /ua1 /B1B2 xsf; move: bg2 => [[[fa _] _] _ fc]; Wtac.
set g3 := Lf (fun x => (Vf g2' (ordinals r1 x))) E1 E2.
have isoc: order_morphism g3 (ordinal_o E1) (ordinal_o E2).
  move: ub1 ub3 => [pa _ _ pb] [_ pc _ pd].
  split => //.
    by rewrite !ordinal_o_sr /g3; hnf; aw; split => //; apply:lf_function.
  hnf;rewrite /g3; aw => x y xe1 ye1; aw.
  move: (pb x y); aw => h; move: (h xe1 ye1).
  set x' := (ordinals r1 x); set y' := (ordinals r1 y) => hh.
  have x'b2: inc x' B2 by apply/B1B2 /ua1.
  have y'b2: inc y' B2 by apply/B1B2 /ua1.
  move:(pd x' y'); rewrite sg2 => h'; move: (h' x'b2 y'b2) => hh'.
  apply: (iff_trans hh); split => //.
    by move => /graph_on_P1 [_ _ ok]; apply /hh' /graph_on_P1.
  move/hh' /graph_on_P1 => [_ _ ok]; apply /graph_on_P1.
  by split => //; apply:ua1.
set g4 := Lf id E1 E2.
have isod : order_morphism g4 (ordinal_o E1) (ordinal_o E2).
  move: isoc => [pa pb _ _]; split => //.
    rewrite !ordinal_o_sr /g4; hnf; aw; split => //; apply: lf_function => //.
  red;rewrite /g4; aw => x y xe1 ye1; aw; split => //.
      move => /graph_on_P1 [_ _ ok]; apply /graph_on_P1.
     by split => //; apply:E1E2.
  by move /graph_on_P1 => [_ _ ok]; apply /graph_on_P1.
have wo2: worder (ordinal_o E2) by apply: ordinal_o_wor.
have wo1: worder (ordinal_o E1) by apply: ordinal_o_wor.
have s1: segmentp (ordinal_o E2) (range (graph g3)).
   move: isoc=> [ _ _ [fg3 sg3 tg3] _].
   split.
     move => t /(range_fP fg3); rewrite - tg3; move => [ x xe1 ->]; Wtac.
   move => x y /(range_fP fg3) [x1 x1s ->] l2.
   have xe1: inc x1 E1 by move:x1s; rewrite sg3 ordinal_o_sr.
   move /ordo_leP: (l2) => [ye2 gx ll]; apply /(range_fP fg3).
   have ve2: inc (Vf g3 x1) E2 by rewrite /g3; aw; apply: sa.
   move: ub2 => [_ _ [bg sg tg2] h2]; move: (h2 y (Vf g3 x1)); aw => h3.
   move /(h3 ye2 ve2): l2.
   have inc1: inc (ordinals r1 x1) B1 by apply :ua1.
   have eq2: (ordinals r2 (Vf g3 x1)) = ordinals r1 x1.
     transitivity (Vf g2 (Vf g3 x1)); first by rewrite /g2; aw.
     by rewrite /g3; aw; apply: inverse_V => //; rewrite tg2 sr2; apply /B1B2.
   rewrite eq2; move /graph_on_P1=> [sa1 sb1 sc1].
   move: ub1=> [_ _ [bg1 sg1 tg1] _].
   have y'b1: inc (ordinals r2 y) (target (Lf (ordinals r1) E1 B1)).
       rewrite tg1 sr1 iv; apply /setI2_P; split => //.
       move: (proj1 cf1 _ inc1) => /(ord_ltP oe1) lt2.
       apply /(ord_ltP oe1); ord_tac.
   have eq3: (ordinals r2 y) = Vf g2 y by rewrite /g2; aw.
   move: (proj2 (proj2 bg1) _ y'b1) => [z]; rewrite lf_source => ze1; aw.
   move => zv; rewrite /g3; aw; exists z => //; aw.
   by rewrite zv eq3 inverse_V2 // sg ordinal_o_sr.
have s2:segmentp (ordinal_o E2) (range (graph g4)).
  have rg4: (range (graph g4)) = E1.
    move: isod=> [ _ _ [fg4 _ _] _].
    set_extens t.
      move/(range_fP fg4); rewrite /g4; aw; move => [x xsf ->]; aw.
    move => xe1; apply/(range_fP fg4); rewrite /g4; aw; ex_tac; aw.
  red; rewrite rg4 ordinal_o_sr; split => // x y xe1 /graph_on_P1 [ye2 _ xy].
  have yx: y <=o x by split => //; ord_tac.
  have xE: x <o E1 by apply /ord_ltP => //.
  apply /ord_ltP => //; ord_tac.
move: (isomorphism_worder_unique wo1 wo2 s1 s2 isoc isod) => g3g4.
hnf; rewrite sf1 sf2; split => // x xe1.
have xe2 := (E1E2 _ xe1).
rewrite /f1 /f2 /ordinalsE; aw; rewrite -/r1 -/r2.
move: ub2 => [_ _ [bg _ tg] _].
have tg2: target g2 = B2 by move: tg; rewrite -/g2 sr2.
move: (f_equal (Vf^~ x) g3g4); rewrite /g3 /g4; aw => eq1.
move: (f_equal (Vf g2) eq1); rewrite {2} /g2; aw.
by rewrite inverse_V //; rewrite tg2; apply /B1B2/ ua1.
Qed.

Definition ordinalsf (p: property) :=
   ordinals (fun x y => [/\ p x, p y & x <=o y]).

Lemma ordinals_col_p1 (p: property) (f := ordinalsf p):
   (forall x, p x -> ordinalp x) -> (non_coll p) ->
 [/\
    forall a, ordinalp a -> p (f a),
    forall x, p x -> exists2 a, ordinalp a & x = f a,
    forall a b, a<=o b -> (f a) <=o (f b),
    forall a b, a<o b -> (f a) <o (f b) &
    (forall a b, ordinalp a -> ordinalp b -> (a<=o b <-> (f a) <=o (f b))) /\
    forall a b, ordinalp a -> ordinalp b -> (a<o b <-> (f a) <o (f b))].
Proof.
move => pa pb.
set r := (fun x y => [/\ p x, p y & x <=o y]).
have pc: (non_coll (fun x => r x x)).
  move => [E Ep]; case: pb; exists E => x; split; first by move /Ep => [].
  move => px; apply /Ep; split => //; move: (pa _ px) => ox; ord_tac.
move: (worder_rc_op p) => pd.
have le0: forall a, ordinalp a -> p (f a).
  by move => a oa; move: (ordinals_Mle pd pc (ord_leR oa)) => [].
have lt1: forall a b, a <o b -> (f a) <o (f b).
  by move => a b h; move: (ordinals_Mlt pd pc h) => [[_ _]].
have le1: forall a b, a<=o b -> (f a) <=o (f b).
  by move => a b h; move: (ordinals_Mle pd pc h) => [_ _].
have lt2:forall x, p x -> exists2 a, ordinalp a & x = f a.
  move => x px.
  have h: r x x by split => //; move: (pa _ px) => ox; ord_tac.
  move:(ordinalsrP pd h) (OS_ordinalr pd h); rewrite -/r -/f => h1 h2.
  by exists (ordinalr r x).
split => //; split.
  move => a b oa ob; split => h; first by apply: le1.
  case: (ord_le_to_el oa ob) => // /lt1 cp; ord_tac.
move => a b oa ob; split => h; first by apply: lt1.
case: (ord_le_to_el ob oa) => // /le1 cp; ord_tac.
Qed.

Lemma ordinals_col_p2 (p: property) (f := ordinalsf p):
   (iclosed_collection p) -> non_coll p ->
   normal_ofs f.
Proof.
move => [pa pb] pc.
set r := (fun x y => [/\ p x, p y & x <=o y]).
move: (ordinals_col_p1 pa pc); rewrite -/r -/f; move => [s1 s2 s3 s4 [s5 s6]].
split=> // a la.
move: (la) => [oa zea lla].
set F :=(fun_image a f).
have nef: nonempty F by exists (f \0o); apply /funI_P; exists \0o.
have Fp: (forall x, inc x F -> p x).
  move => t /funI_P[z za ->]; apply:s1; ord_tac.
have osF: ordinal_set F by move => t /Fp/pa.
move: (pb _ Fp nef) => puF.
have bfa : ordinal_ub F (f a).
  by move => t /funI_P [z /(ord_ltP oa) [za _] ->]; apply:s3.
have ofa: ordinalp (f a) by apply: (pa _ (s1 _ oa)).
move: (ord_ub_sup osF ofa bfa).
move: (s2 _ puF) => [b ob bv]; rewrite bv => p1.
case: (ord_le_to_ell oa ob) => cab; first by rewrite cab.
  move:(s4 _ _ cab) => [lfab _]; ord_tac.
move:(s4 _ _ (ord_succ_lt ob)) => h.
have sb: succ_o b <o a by move /(limit_ordinal_P3): la => [ _]; apply.
have sbb: inc (succ_o b) a by apply /(ord_ltP oa).
have: inc (f (succ_o b)) F by apply/funI_P; ex_tac.
move /(ord_sup_ub osF); rewrite bv=> h1; ord_tac.
Qed.

Definition first_derivation (f: fterm) :=
  (ordinalsf (fun z => ordinalp z /\ f z = z)).

Lemma iclosed_col_f0 (p: property) (f := ordinalsf p) (x:= f \0o):
  (iclosed_collection p) -> (non_coll p) ->
  (p x /\ (forall z, p z -> x <=o z)).
Proof.
move => [pa pb] pc.
set r := (fun x y => [/\ p x, p y & x <=o y]).
move: (ordinals_col_p1 pa pc); rewrite -/r -/f; move => [s1 s2 s3 s4 [s5 s6]].
split; first by apply: s1; fprops.
move => z /s2 [a oa ->]; apply: s3; ord_tac1.
Qed.

Lemma iclosed_col_fs (p: property) (f := ordinalsf p) a
   (x:= f a) (y := f (succ_o a)) :
  (iclosed_collection p) -> (non_coll p) -> ordinalp a ->
  [/\ x <o y, p x, p y & (forall z, p z -> x <o z -> y <=o z)].
Proof.
move => [pa pb] pc oa.
set r := (fun x y => [/\ p x, p y & x <=o y]).
move: (ordinals_col_p1 pa pc); rewrite -/r -/f; move => [s1 s2 s3 s4 [s5 s6]].
move:(OS_succ oa) => ob.
move: (s4 _ _ (ord_succ_lt oa)) => h; split => //; try apply: s1 => //.
move => z /s2 [c oc -> fc].
by apply/(s5 (succ_o a) c ob oc) /ord_succ_ltP /(s6 _ _ oa oc).
Qed.

Lemma first_derivation_p f (fp := first_derivation f): normal_ofs f ->
  ( (forall x, ordinalp x -> f (fp x) = fp x) /\
    (forall y, ordinalp y -> f y = y -> exists2 x, ordinalp x & y = fp x)).
Proof.
move => pa.
move:(iclosed_fixpoints pa).
pose p z :=(ordinalp z /\ f z = z).
have sa: (forall x, p x -> ordinalp x) by move => x [].
rewrite /fp /first_derivation -/p.
move => [sc sd].
move:(ordinals_col_p1 sa sd) => [pb pc pd pe [pf pg]].
by split; [move => x /pb [_] | move => y oy fy; apply:pc ].
Qed.

Lemma first_derivation_p0 f: normal_ofs f ->
  normal_ofs (first_derivation f).
Proof.
by move /iclosed_fixpoints => [pa pb]; exact (ordinals_col_p2 pa pb).
Qed.

Lemma first_derivation_p1 f: normal_ofs f ->
  (first_derivation f \0o) = the_least_fixedpoint_ge f \0o.
Proof.
move => nf; move:(iclosed_fixpoints nf) => [pa pb].
set p := (fun z => ordinalp z /\ f z = z).
have pc: forall x, p x -> ordinalp x by move=> x [].
move: (ordinals_col_p1 pc pb) => [q1 q2 q3 q4 [q5 q6]].
rewrite /first_derivation -/p.
move: (normal_ofs_fix nf OS0) => [sa sb sc].
apply: ord_leA.
  move: (q2 _ (conj (proj32 sa) sb)) => [a oa ->]; apply: q3; ord_tac1.
move: (q1 _ OS0) => [/ozero_least ha hb]; exact (sc _ ha hb).
Qed.

Lemma first_derivation_p2 f: normal_ofs f -> f \0o <> \0o ->
  (first_derivation f \0o) = the_least_fixedpoint_ge f \1o.
Proof.
move => nf nf0; move:(iclosed_fixpoints nf) => [pa pb].
set p := (fun z : Set => ordinalp z /\ f z = z).
have pc: forall x, p x -> ordinalp x by move=> x [].
move: (ordinals_col_p1 pc pb) => [q1 q2 q3 q4 [q5 q6]].
rewrite /first_derivation -/p.
move: (normal_ofs_fix nf OS1) => [sa sb sc].
apply: ord_leA.
  move: (q2 _ (conj (proj32 sa) sb)) => [a oa ->]; apply: q3; ord_tac1.
move: (q1 _ OS0) => [/ozero_least ha hb]; apply: sc => //.
by apply: ord_ge1; [ ord_tac |move => ba; case: nf0; rewrite - ba].
Qed.

Lemma first_derivation_p3 f x: normal_ofs f -> ordinalp x ->
  (first_derivation f (succ_o x)) =
    the_least_fixedpoint_ge f (succ_o (first_derivation f x)).
Proof.
move => nf ox; move:(iclosed_fixpoints nf) => [pa pb].
set p := (fun z : Set => ordinalp z /\ f z = z).
have pc: forall y, p y -> ordinalp y by move=> y [].
move: (ordinals_col_p1 pc pb) => [q1 q2 q3 q4 [q5 q6]].
rewrite /first_derivation -/p.
move: (q1 _ ox) => [ta tb].
move: (normal_ofs_fix nf (OS_succ ta)) => [/ord_succ_ltP sa sb sc].
apply: ord_leA.
  move: (q2 _ (conj (proj32_1 sa) sb)) => [a oa av].
  case:(ord_le_to_el oa ox); first by move /q3; rewrite - av => l1; ord_tac.
  by rewrite av; move /ord_succ_ltP /q3.
move: (q1 _ (OS_succ ox)) => [ua ub];apply: sc => //; apply /ord_succ_ltP.
by apply: q4; apply: ord_succ_lt.
Qed.

Lemma normal_ofs_from_exten f g : f =1o g -> normal_ofs f -> normal_ofs g.
Proof.
move => h [sa sb].
split => //.
  move => x y xy; move: (xy)=> [[ox oy _]_].
 by rewrite - h // - h //; apply: sa.
move => x lx; move: (proj31 lx) => ox.
rewrite -(h x ox) (sb _ lx).
apply: ord_sup_2funI => t tx; apply: h; ord_tac.
Qed.

Lemma first_derivation_exten f g : f =1o g -> normal_ofs f ->
 first_derivation f =1o first_derivation g.
Proof.
move => h osf.
have osg := (normal_ofs_from_exten h osf).
move:(first_derivation_p osf) => [sa sb].
move:(first_derivation_p osg) => [sc sd].
move: (first_derivation_p0 osf) (first_derivation_p0 osg) => [ia _] [ib _].
apply: (sincr_ofs_exten ia ib).
move => x ox.
  have ha: ordinalp (first_derivation f x) by apply: ofs_sincr.
  by apply: sd => //;rewrite - h //;apply: sa.
move => x ox.
  have ha: ordinalp (first_derivation g x) by apply: ofs_sincr.
  by apply: sb => //;rewrite h //;apply: sc.
Qed.

Lemma first_derivation_p4 f C (E:= succ_c C) (f' := first_derivation f)
   (F := Zo E (fun z => f z = z)):
   infinite_c C ->
   normal_ofs f ->
   (forall x, inc x E -> inc (f x) E) ->
   order_isomorphism (Lf f' E F) (ordinal_o E) (graph_on ordinal_le F).
Proof.
move => iC nf fse;move: (iC) => [cC _].
move:(succ_c_pr1 cC); rewrite -/E; move=> [pa pb pc].
move: (iclosed_fixpoints nf)=> [pa' pb'].
move: (ordinals_col_p2 pa' pb') => nf'.
set p := (fun z : Set => ordinalp z /\ f z = z).
have pc': forall x, p x -> ordinalp x by move=> x [].
move: (ordinals_col_p1 pc' pb').
have -> : ordinalsf p = f' by [].
move => [q1 q2 q3 q4 [q5 q6]].
move: (proj1 pa) => oe.
have oes: forall x, inc x E -> ordinalp x by move => x xE; ord_tac.
set g := Lf f' E F.
have sa: forall a b, inc b E -> a <o b -> inc a E.
  move => a b /(ord_ltP oe) ha hb; apply/(ord_ltP oe); ord_tac.
have lfa: lf_axiom f' E F.
  move => x xE; move: (oes _ xE) => ox; move:(q1 _ ox) => [_ aa].
  apply: Zo_i => //; clear aa; ex_middle bad.
  pose P x := inc x E /\ ~ inc (f' x) E.
  have px: P x by [].
  move: (least_ordinal4 ox px); set z := least_ordinal _ _.
  move => [oz [zE ney] el]; case: ney.
  move:(oes _ zE) => ozz.
  have ell: forall t, t <o z -> inc (f' t) E.
    move => t tz; move: (proj31_1 tz) => ot.
    case: (p_or_not_p (P t)); first by move => /(el _ ot) => zt; ord_tac.
    move => pt; ex_middle ba;case: pt; split => //; apply: (sa _ _ zE tz).
  move: (next_fix_point_small iC nf fse) => H.
  case: (limit_ordinal_pr2 oz).
      move => ->; rewrite /f' (first_derivation_p1 nf); apply: H.
      apply succ_cP => //; split; rewrite ? (card_card CS0); fprops.
    move => [t ot te]; rewrite te.
    rewrite /f' (first_derivation_p3 nf ot); apply: H.
    by apply:(succ_c_succ iC); apply: ell; rewrite te; apply: ord_succ_lt.
  move => lz; move: (proj2 nf' _ lz).
  set w := ordinalsf _ ; have -> : w = f' by []; clear w.
  move => ->; apply: (succ_c_sup iC).
    move /(succ_cP cC): zE => [_]; apply: card_leT.
    exact: (fun_image_smaller z f').
  move => t /funI_P [u uz ->]; apply:ell; ord_tac.
split.
- apply: ordinal_o_or.
- apply: order_from_rel; apply:ordinal_le_order_r.
- split.
  + apply: lf_bijective.
   - done.
   - move => u v /oes ou /oes ov sv.
     by case: (ord_le_to_ell ou ov) => // /q4 []; rewrite sv.
   - move => y /Zo_P [ye yv]; move: (q2 _ (conj (oes _ ye) yv)) => [a a1 a2].
     exists a => //; move: (osi_gex q4 a1); rewrite - a2.
     move /(ord_ltP oe): ye => ha hb; apply/(ord_ltP oe); ord_tac.
- rewrite ordinal_o_sr /g; aw.
  rewrite graph_on_sr /g ; aw => a /Zo_P [/oes oa _]; ord_tac.
- red;rewrite /g;aw; move => x y xE yE; aw; split.
    move /sub_gleP => [_ _ xy]; apply /graph_on_P1; split; fprops.
    apply: q3; split; fprops.
 move /graph_on_P1 => [_ _] /(q5 _ _ (oes _ xE) (oes _ yE)) [_ _ xy].
 by apply /sub_gleP.
Qed.

Lemma ord_rev_pred x (y:= x -o \1o) : \0o <o x->
   (ordinalp y /\ x = \1o +o y).
Proof. by move /ord_ge1P => /odiff_pr. Qed.

Lemma rev_pred_prop (f := fun z => \1o +o z):
  normal_ofs f /\ (forall y, \0o <o y -> exists2 x, ordinalp x & y = f x).
Proof.
split; first apply: (osum_normal OS1).
by move => y /ord_rev_pred [pa pb]; exists (y -o \1o); rewrite /f.
Qed.

Lemma non_zero_ord_enum:
  (fun z => \1o +o z) =1o ordinalsf (fun x => \0o <o x).
Proof.
set p := (fun x => \0o <o x).
have pa :(iclosed_collection p).
  split; first by move => x [] h _; ord_tac.
  move => F hx [t tx].
  have osf: ordinal_set F by move => x /hx [h _]; ord_tac.
  move: (ord_sup_ub osf tx); apply: ord_lt_leT; exact (hx _ tx).
have pb: (non_coll p).
   rewrite /p;move=>[E xe].
   have ose: ordinal_set E by move => t /xe h; ord_tac.
   move: (OS_sup ose) => sse.
   move: (ord_lt0_succ (OS_sup ose)) => /xe se.
   by move:(ord_sup_ub ose se) => /ord_succ_ltP [].
move => t ot.
apply:(normal_ofs_uniqueness (p:= fun z => z+o \1o)).
- apply: (osum_normal OS1).
- by apply: (ordinals_col_p2 pa pb).
- by move => x ox; rewrite - (ord_succ_pr ox) (osumA OS1 ox OS1).
- move => x /(iclosed_col_fs pa pb).
  set u := ordinalsf p x; set v := ordinalsf p (succ_o x).
  rewrite /p;move =>[/ord_succ_ltP uv [[_ ou _] _] _ h].
  rewrite (ord_succ_pr ou); apply: ord_leA => //.
  apply: h; [by apply:ord_lt0_succ| by apply:ord_succ_lt].
- move: (iclosed_col_f0 pa pb); set u := ordinalsf p \0o.
  rewrite (osum0r OS1); move => [] /ord_ge1P u1 h.
  move: (h _ (ord_lt_01)) => h'; ord_tac.
- exact.
Qed.

Lemma add1_fix_enumeration:
  first_derivation (ord_sum2 \1o) =1o (ord_sum2 omega0).
Proof.
move: OS1 OS_omega => o1 oo.
move: (osum_normal o1) (osum_normal oo) => np1 npo.
move: (iclosed_fixpoints np1); move => [pa pb].
move:(ordinals_col_p2 pa pb) => na.
set (p:= fun z => ordinalp z /\ \1o +o z = z).
have pc: forall x, p x -> omega0 <=o x by move => x [p1 /(oadd1_fix p1)].