proposition: Lemma olim_supinf_prop f b: \0o <o b -> ord_below_b f b -> oliminf f b <=o olimsup f b.
proof: Proof. move => lob ofs. have ob:= proj32_1 lob. have H := ointvP ob. rewrite /olimsup; set E := fun_image _ _. have neE: nonempty E by apply: funI_setne; move/(oltP ob): lob => 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. apply: (ord_ub_sup oa) => v /funI_P [j /(oltP ob) ljb ->]. set F := fun_image _ _. have neF: nonempty F. apply: funI_setne; exists j; apply /H; split => //. exact: (oleR (proj31_1 ljb)). have osF: ordinal_set F. by move => x /funI_P [i /H /proj2 /ofs h ->]. move: (least_ordinal0 osF neF); set c := intersection F; move => [oc cf cp]. move: (omax_p1 (proj31_1 ljb) (proj31_1 lkb)). set n := omax j k; move => [nj nk]. have nb : n <o b by rewrite /n/omax/Gmax; Ytac h. have /cp le1: inc (f n) F by apply: funI_i; apply/H. by apply(oleT le1); apply: (ord_sup_ub osU); apply: funI_i; apply/H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)