proposition: Lemma olimit_example (f := fun i => i %%c \2c) (x := omega0): ord_below_b f x /\ forall l, olimit f x l -> False.
proof: Proof. split. by move => i /(oltP OS_omega) ilo; apply: OS_nat; apply: NS_rem. move => l [[y /(oltP OS_omega) yN yq] lb]. have fe i: natp i -> f (cdouble i) = \0o by case/even_double. have fo i: natp i -> f (csucc(cdouble i)) = \1o. by move => /odd_succ_double/oddp_alt []. move:(NS_succ (NS_double yN)); set z := (csucc _) => zN. have zx: z <o x by apply /(oltP OS_omega). move: (oclt (cle_ltT (cle_n_doublen yN) (cltS (NS_double yN)))) => ylz. move: (yq z (proj1 ylz) zx); rewrite (fo _ yN) => /oge1P lp. move:(lb \0o lp) => [y1 /(oltP OS_omega) y1N yr]. have y2N := NS_succ y1N. move: (proj1 (oclt (clt_leT (cltS y1N) (cle_n_doublen y2N)))) => la. move/(oltP OS_omega): (NS_double y2N) => lc. by move: (yr _ la lc); rewrite (fe _ y2N); case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)