proposition: Lemma cont_fun_th4_ex1 a b (f := fun i x => Yo (x <=o i) a b) (g := fun x => Yo (x <o omega0) a b): a <o b -> [/\ forall i x y, ordinalp i -> x <=o y -> f i x <=o f i y, 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: (lab) => [[oa ob _] _]. split. - move: (proj1 lab) => leab; move: (leab) => [/oleR oea /oleR oeb _]. move => i x y oi lxy; rewrite /f; Ytac h1; Ytac h2 => //. by case: h1; apply: (oleT lxy h2). - move => i x oi limx; rewrite /ocontinuous_at /f. Ytac lxi. apply: (olimit_econst oa). exists \0o; first by apply: limit_pos. by move => j _ jx; rewrite (Y_true (oleT (proj1 jx) lxi)). case: (oleT_el (proj31 limx) oi) => // lt. apply: (olimit_econst ob); exists (osucc i). by move/limit_ordinal_P: limx => [_]; apply. by move => j /oleSltP /oltNge ja jb; Ytac0. - move => x ox; rewrite /g; Ytac h. apply: (olimit_econst oa); exists x => //. by move => i ia ib; rewrite /f; Ytac0. apply: (olimit_econst ob); exists \0o; first by apply: olt_0omega. move => i _ ia; rewrite /f; Ytac hh => //; case: h; exact:(ole_ltT hh ia). - move => [qa qb]. move: qb; rewrite /g Y_false; last by case. move => h1; move: (h1 a lab) => [y lyo h2]. by move: (h2 y (oleR (proj31_1 lyo)) lyo); Ytac0; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)