proposition: Lemma cont_fun_th1_bis (f: fterm) b: b <o aleph1 -> ord_below_b f aleph1 -> exists F, cont_fun_th3_prop f b F.
proof: Proof. move => ba ha. move: OS_omega (proj32_1 ba) => oo oo1. move: (aleph_limit OS1) ; rewrite -/aleph1. move/limit_ordinal_P => /proj2 h; move:(h _ ba) => sba; clear h. have hb:ord_below_b f (osucc b). by move => t lt; apply: ha; apply: (olt_ltT lt sba). move: (cont_fun_th1 sba hb) => [F [fa fb fc]]. pose g i x := Yo (x <=o b) (F i x) \0o. pose G := Lg (omega0 \times aleph1) (fun p => g (P p) (Q p)). have ra: fgraph G by rewrite/G; fprops. have rb: domain G = omega0 \times aleph1 by rewrite Lgd. have pd 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. have rc1: allf G ordinalp. move => t; rewrite rb /G/g => tp; rewrite LgV//; Ytac h; last by apply: OS0. move/setX_P: tp => [qa /(oltP oo) qb qc]. apply: fa => //. by apply/oltSleP. have rc2 i x: i <o omega0 -> b <o x -> x <o aleph1 -> Vg G (J i x) = \0o. move => ua /oleNgt ub uc; move: (pd _ _ ua uc) => pp. rewrite /G/g LgV//; aw; rewrite Y_false => //. have rd x: x <=o b -> olimit (fun i => Vg G (J i x)) omega0 (f x). move => lxb. have lesb: x <o osucc b by apply/oltSleP. move: (fc _ lesb). have sb: (esame_below (F^~ x) (fun i => Vg G (J i x)) omega0). exists \0o; first by apply: olt_0omega. move => t tplto to /=. move: (pd _ _ to (ole_ltT lxb ba)) => aux. by rewrite /G/g LgV//; aw; Ytac0. by move/ (olim_exten _ sb). exists G; split => //. move => i lio x limx lxa. move:(pd _ _ lio lxa) => dp9. rewrite /ocontinuous_at {2}/G /g LgV//; aw; Ytac h. have lxb: x <o (osucc b) by apply/oltSleP. move: (fb _ lio _ limx lxb). have sb: (esame_below [eta F i] (fun x0 : Set => Vg G (J i x0)) x). exists \0o; first by apply: limit_pos. move => t _ ltx; move:(pd _ _ lio (olt_ltT ltx lxa)) => dp. by rewrite /G/g LgV//; aw; rewrite (Y_true (oleT (proj1 ltx) h)). by move/ (olim_exten _ sb). case:(oleT_el (proj31_1 lxa) (proj31_1 ba)) => // lbx. move/limit_ordinal_P: limx => /proj2 q; move:(q _ lbx) => sbx; clear q. apply/olimit_zero; exists (osucc b) => // j ja jb. move: (pd _ _ lio (olt_ltT jb lxa)) => pp. by rewrite /G/g LgV //;aw; rewrite Y_false //; apply:oltNge; apply/oleSltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)