proposition: Lemma non_cont_ex4 (x := omega0 ^o \2o +o omega0): limit_ordinal x /\ ocontinuous_at (fun t => t +o t) x.
proof: Proof. move:(opow_Mo_lt olt_12)(indecomp_prop4 OS2); rewrite oopow1. set a := oopow \2o => ha hb. move: omega_limit OS_omega (proj32_1 ha) => lo oo oa. move: (osum_limit oa lo) => lx; split => //. pose f t := t +o t. have h i j: i <=o j -> j <o x -> f i <=o f j. move => sa _; apply: (osum_Mlele sa sa). move:(olim_sup lx h). set A := fun_image _ _; set b := \osup _. suff : b = x +o x by move ->. have ox := (proj31 lx). have osA: ordinal_set A. by move => y /funI_P [i /(oltP ox ) /proj31_1 la ->]; apply: OS_sum2. have: b <=o x +o x. apply: (ord_ub_sup (OS_sum2 ox ox)) => z /funI_P [i /(oltP ox) ll -->]. exact: (osum_Mlele (proj1 ll)(proj1 ll)). case /ole_eqVlt => //. have fs t: t <o a -> f (a +o t) = (a +o a) +o t. move => ta; move: (proj31_1 ta) => ot; move:(OS_sum2 oa ot) => oat. by rewrite /f (osumA oat oa ot) -(osumA oa ot oa) (indecomp_prop1 hb ta). rewrite -/(f x) (fs omega0 ha) => bs. have aA: inc (a +o a) A. apply: funI_i; apply/(oltP ox). by move: (osum_Meqlt olt_0omega oa); rewrite (osum0r oa). move: (ord_sup_ub osA aA) => leb. move: (odiff_pr leb); set c := _ -o _; move =>[oc cv]. case: (oleT_el oo oc) => cs. by case (oltNge bs); move:(osum_Meqle cs (OS_sum2 oa oa)); rewrite - cv. suff bA: inc (osucc b) A by move: (ord_sup_ub osA bA) => /oleSltP; case. move/limit_ordinal_P:omega_limit =>[ _ ho]; move: (ho _ cs) => scs. apply/funI_P; exists (a +o osucc c). by apply/(oltP ox); apply: osum_Meqlt. by rewrite (fs _ (olt_ltT scs ha)) - (osum2_succ (OS_sum2 oa oa) oc) - cv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)