proposition: Lemma normal_ofs_existence (p:fterm) a (osup := fun f => \osup (fun_image (domain f) (fun z => (p (Vg f z))))) (osupp:= fun f => Yo (domain f = \0o) a (osup f)) (f:= transdef_ord osupp): (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 (osucc x) = p (f x)) ].
proof: Proof. move => incrp pi oa. have f0: f \0o = a. by rewrite /f(transdef_ord_pr osupp OS0) /osupp; aw; Ytac0. have frec3 :forall y, \0o <o y -> f y = \osup (fun_image y (fun z => p (f z))). move => y [[_ oy _] ynz]; rewrite {1}/f (transdef_ord_pr osupp oy)/osupp. by rewrite -/f/osup; aw; Ytac0; apply: ord_sup_2funI => t ty; rewrite LgV. have frec4: forall x, ordinalp x -> ordinalp (f x). apply: least_ordinal2' => x ox hr. case: (ozero_dichot ox); first by move ->; ue. move/frec3 => ->; apply:OS_sup => t /funI_P [z sa ->]. exact:(proj32_1 (incrp _ (hr _ sa))). have frec5: forall x y, x <o y -> p (f x) <=o f y. move => x y xy. have oy:= (proj32_1 xy). have ixy:= (olt_i xy). have yp:= (ole_ltT (ole0x (proj31_1 xy)) xy). rewrite (frec3 _ yp); apply: ord_sup_ub;last by apply /funI_P; ex_tac. by move => t /funI_P [z /(Os_ordinal oy) /frec4 /incrp [[_ h _] _] ->]. have frec6: forall x y, x <o y -> (f x) <o f y. move => x y xy; move: (frec5 _ _ xy) => l1. exact: (olt_leT (incrp _ (frec4 _ (proj31_1 xy))) l1). have frec7:forall x, ordinalp x -> f (osucc x) = p (f x). move => x ox. have xsx: x <o osucc x by apply: oltS. apply: oleA (frec5 _ _ xsx). have osx:= (OS_succ ox). rewrite (frec3 _ (olt0S ox)) /osup;apply: ord_ub_sup. - by move:(incrp _ (frec4 _ ox)) => [[]]. - move => t /funI_P [z zx ->]; apply: pi. case/setU1_P: zx; last by move ->; exact: (oleR (frec4 _ ox)). by move /(oltP ox) => /frec6 []. split => //; split =>// x lx; move:(proj31 lx) => ox. rewrite (frec3 _ (limit_pos lx)). have hz: forall z, inc z x -> z <o osucc z. move => z zx ;apply: (oltS (Os_ordinal ox zx)). apply: ord_sup_2cofinal;split; move => c /funI_P [z zx ->]; move:(hz _ zx)=> ht. move:(proj33 lx _ zx) => h; exists (f (osucc z)); last by apply:frec5. apply /funI_P; ex_tac. exists (f (osucc z)); first by apply/funI_P; ex_tac; apply: frec7 (proj31_1 ht). by case: (frec6 _ _ ht). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)