proposition: Lemma cont_fun_th4_ex2 a b (f := fun i x => Yo (i <o x /\ x <=o omega0) a b) (g := fun x => Yo (x = omega0) a b): a <o b -> [/\ forall i j x, i <=o j -> ordinalp x -> f i x <=o f j x, forall i x, ordinalp i -> limit_ordinal x -> ocontinuous_at (f i) x, forall x, ordinalp x -> olimit (fun i => f i x) omega0 (g x) & ~ocontinuous_at g omega0].
proof: Proof. move => lab; move: (proj1 lab) => leab. move: (leab) => [oa ob _]; move: (oleR oa) (oleR ob) => laa lbb. split. - move => i j x lij ox; rewrite /f. case: (oleT_el ox OS_omega) => ll; last first. by move:(oltNge ll) => ngr; rewrite ! Y_false => //; case. case: (p_or_not_p (j <o x)) => ljx. by rewrite (Y_true (conj ljx ll)) (Y_true (conj (ole_ltT lij ljx) ll)). have aux: ~ (j <o x /\ x <=o omega0) by case. by Ytac0; Ytac h2. - move => i x oi lx; rewrite /f/ocontinuous_at. case: (oleT_el (proj31 lx) oi) => lix. rewrite Y_false;last by case =>q; case:(oleNgt lix). apply: (olimit_econst ob). exists \0o; first by apply: limit_pos. move => j ja jb; rewrite Y_false //; case => ji _. by move:(oleNgt (oleT (proj1 jb) lix) ji). case: (oleT_el (proj31 lx) OS_omega) => lxo. rewrite (Y_true (conj lix lxo)). apply: (olimit_econst oa). exists (osucc i). by move/limit_ordinal_P: lx => [_ h]; move: (h _ lix). move => k /oleSltP ka kb; rewrite Y_true => //;split => //. apply: (oleT (proj1 kb) lxo). move: (oltNge lxo) => nlxo. rewrite Y_false; last by case. apply: (olimit_econst ob); exists (osucc omega0). by move/limit_ordinal_P: lx => [_ h]; move: (h _ lxo). by move => k /oleSltP /oltNge ka kb;rewrite Y_false => //; case. - move => x ox; rewrite /g. case: (oleT_ell ox OS_omega) => cxo. + Ytac0; apply:(olimit_econst oa). exists \0o; first by apply: olt_0omega. move => i ia ib; rewrite /f cxo Y_true => //; split => //. apply: (oleR OS_omega). + rewrite (Y_false (proj2 cxo)); apply:(olimit_econst ob). exists x => //. by move => k /oleNgt ka kb; rewrite /f Y_false => //; case. + rewrite (Y_false (nesym (proj2 cxo))); apply:(olimit_econst ob). exists \0o; first by apply: olt_0omega. move => i ia ib; rewrite /f Y_false => //; case => _. exact:(oltNge cxo). - rewrite /ocontinuous_at /g; Ytac0; move => [ha hb]. move:ha =>[y yo yp]; move: (yp y (oleR (proj31_1 yo)) yo). by rewrite (Y_false (proj2 yo)); apply: (oltNge lab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)