proposition: Lemma normal_ofs_bounded x f: ordinalp x -> normal_ofs f -> x <o f \0o \/ exists y, [/\ ordinalp y, f y <=o x & x <o f (osucc y)].
proof: Proof. move=> ox [pa pb]. move: (osi_gex1 pa ox) => [y [oy xle ymin]]. case: (equal_or_not x (f y)) => xo. have lt1:= (pa _ _ (oltS oy)). rewrite xo;right; exists y; split => //; apply: (oleR (proj32 xle)). have xlt: x <o f y by split. case: (ordinal_limA oy). by move => ye; move: xlt; rewrite ye => xx; left. move => [z oz yz]; rewrite yz in oy. right; exists z; rewrite -yz;split => //. move: (oltS oz); rewrite -yz => le3. move: (pa _ _ le3) => [[ofz _] _]. case: (oleT_ee ofz ox) => //. move=> le1; case: (oleNgt (ymin _ oz le1) le3). move => li; move: xlt; rewrite (pb _ li) => xu. have os: ordinal_set (fun_image y f). apply:Os_funI => z /(Os_ordinal oy) oz. exact: (ofs_sincr pa oz). move: (olt_sup os xu) => [z /funI_P [t ty ->] le2]. have yt: t <o y by apply /(oltP oy). case: (oleNgt (ymin _ (Os_ordinal oy ty) (proj1 le2)) yt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)