proposition: Lemma cont_fun_th4_aux (f: fterm2) bi bx (g := fun x => \osup (fun_image bi (fun i => f i x))): limit_ordinal bi -> ordinalp bx -> (forall i j x, i <=o j -> j <o bi -> x <o bx -> f i x <=o f j x) -> (forall i x y, i <o bi -> x <=o y -> y <o bx -> f i x <=o f i y) -> [/\ forall x, x <o bx -> ordinal_set (fun_image bi (f^~ x)), forall x, x <o bx -> olimit (fun i => f i x) bi (g x), (forall x y, x <=o y -> y <o bx -> g x <=o g y) & forall i x, i <o bi -> x <o bx -> f i x <=o g x].
proof: Proof. move => lbi obx inc1 inc2. move /limit_ordinal_P: (lbi) => [bip blim]. move: (proj32_1 bip) => obi. have osa x: x <o bx -> ordinal_set (fun_image bi (f^~ x)). move => xo v /funI_P [i li ->]. move/(oltP obi):li => la; move: (proj31_1 la) => oi. exact: (proj31 (inc1 _ _ _ (oleS oi) (blim _ la) xo)). have ha i x: i <o bi -> x <o bx -> f i x <=o g x. by move => li lx; apply: (ord_sup_ub (osa _ lx)); apply: funI_i; apply/oltP. have og x: x <o bx -> ordinalp (g x). move => h; exact: (proj32 (ha _ _ bip h)). have hb x: x <o bx -> olimit (f^~ x) bi (g x). by move => xl;apply: (olim_sup lbi) => i j qa qb; apply: inc1. split => // x y lxy lyb . apply: (ord_ub_sup (og _ lyb)) => tv /funI_P [i /(oltP obi) si ->]. exact: (oleT (inc2 _ _ _ si lxy lyb) (ha _ _ si lyb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)