proposition: Lemma olim_supinf_prop3 f b l: \0o <o b -> ord_below_b f b -> olimit f b l -> oliminf f b = olimsup f b /\ l = oliminf f b.
proof: Proof. move => bp ofs h. move: (OS_olim h) => ol; move: h => [lfu lfl]. have ob:= proj32_1 bp. have H := ointvP ob. move: (olim_supinf_prop bp ofs) => le1. have le2: olimsup f b <=o l. move: lfu => [k kb etc]. rewrite /olimsup; set E := fun_image _ _. have neE: nonempty E by apply: funI_setne; move/(oltP ob): bp => h; ex_tac. have osE: ordinal_set E. move => v /funI_P [j jb ->]. by apply: OS_sup => u /funI_P[ i /H/proj2 /ofs xx ->]. move:(least_ordinal0 osE neE); set a := intersection _. move =>[oa ap1 ap2]. set u := \osup (fun_image (ordinal_interval k b) f). have: inc u E by apply: funI_i; apply/(oltP ob). move /ap2 => au; apply:(oleT au). by apply (ord_ub_sup ol) => t /funI_P [i /H [ia ib] ->]; apply: etc. case: (ole_eqVlt (oleT le1 le2)) => h. by split => //; apply: oleA => //; rewrite h. move/lfl:h => [i ltib etc]. pose Fj j := (fun_image (ordinal_interval j b) f). have ha j: j <o b -> nonempty (Fj j). move => ljb; apply: funI_setne; exists j; apply/H; split => //. exact: (oleR (proj31_1 ljb)). have hb j: j <o b -> ordinal_set (Fj j). by move => ljb t /funI_P [k /H/proj2/ofs ox ->]. move :(ordinal_setI (ha _ ltib) (hb _ ltib)) => /funI_P [j /H [ja jb] jc]. move: (etc j ja jb); rewrite - jc { etc j ja jb jc} => lt1. pose E := (fun_image b (fun k => intersection (Fj k))). have osE: ordinal_set E. move => t /funI_P [j /(oltP ob) jb ->]. by case:(least_ordinal0 (hb _ jb) (ha _ jb)). have fi: inc (intersection (Fj i)) E by apply: funI_i; apply/(oltP ob). case: (oltNge lt1 (ord_sup_ub osE fi)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)