proposition: Lemma olim_supinf_prop2 f b: \0o <o b -> ord_below_b f b -> oliminf f b = olimsup f b -> olimit f b (oliminf f b).
proof: Proof. move => bp ofs eq1. have ob:= proj32_1 bp. have H := ointvP ob. split. rewrite eq1; 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:(ordinal_setI neE osE) => /funI_P [k /(oltP ob) lkb ->]. set U := fun_image _ _; set a := \osup _. have osU: ordinal_set U. by move => x /funI_P [i /H /proj2 /ofs h ->]. have oa: ordinalp a by apply: OS_sup. exists k => // i i1 i2. by apply: (ord_sup_ub osU); apply: funI_i; apply /H. rewrite /oliminf; set E := fun_image _ _. 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 [i /H/proj2/ofs ox ->]. have osE: ordinal_set E. move => t /funI_P [i /(oltP ob) ilb ->]. by case :(least_ordinal0 (hb _ ilb) (ha _ ilb)). move => l /(olt_sup osE) [z /funI_P[j /(oltP ob) ilb -> ]] h. exists j => // k k1 K2; apply:(olt_leT h). case :(least_ordinal0 (hb _ ilb) (ha _ ilb)) =>[ua ub uc]. by apply: uc; apply: funI_i; apply/H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)