# 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].
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.