proposition: Lemma cont_fun_th3 (f: fterm) (tf := fun a x => Yo (x <=o a) (f x) \0o): ord_below_b f aleph1 -> exists (F: Set -> Set -> Set -> Set), [/\ forall a i x, a <o aleph1 -> i <o omega0 -> x <o aleph1 -> ordinalp (F a i x), forall a i, a <o aleph1 -> i <o omega0 -> ocontinuous_below (fun x => F a i x) aleph1, forall a x, a <o aleph1 -> x <o aleph1 -> olimit (fun i => (F a i x)) omega0 (tf a x) & forall x, x <o aleph1 -> olimit (fun i => (tf i x)) aleph1 (f x)].
proof: Proof. move => ha. move: (aleph_lt_lto olt_01); rewrite -/aleph1 aleph0E => olt01. move: (olt01) => [[oo oo1 _] _]. have H i x: i <o omega0 -> x <o aleph1 -> inc (J i x) (omega0 \times aleph1). by move => /(oltP oo) qa /(oltP oo1) qb; apply: setXp_i. pose Ga a := choose (fun z => cont_fun_th3_prop f a z). have Gap a: a <o aleph1 -> cont_fun_th3_prop f a (Ga a). move =>h; apply: (choose_pr (cont_fun_th1_bis h ha)). pose F := (fun a i x => (Vg (Ga a) (J i x))). have ra a i x: a <o aleph1 -> i <o omega0 -> x <o aleph1 -> ordinalp (F a i x). move => pa pi px; move: (Gap a pa) => [sa sb [sc _] _ _ ]. by apply: sc; rewrite sb; apply:H. have rd x: x <o aleph1 -> olimit (tf^~ x) aleph1 (f x). move => xp; apply: (olimit_econst (ha _ xp)). by exists x => // t xt ta; rewrite /tf; Ytac0. have rb a i: a <o aleph1 -> i <o omega0 -> ocontinuous_below [eta F a i] aleph1. move => pa io x lx xa. move: (Gap a pa) => [_ _ _ se _ ]; exact: (se _ io x lx xa). exists F; split => //. move => a x pa px. move: (Gap a pa) => [ _ sb [sc sd] _ se ]. rewrite /tf; Ytac h; first exact: (se _ h). case: (oleT_el (proj31_1 px) (proj31_1 pa)) => // ax. apply/ olimit_zero; exists \0o; first by apply: olt_0omega. by move => i _ ib; rewrite /F sd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)