proposition: Lemma olim_sup_spec f x y: limit_ordinal x -> y <o x -> (forall i j, y <=o i -> i <=o j -> j <o x -> f i <=o f j) -> olimit f x (\osup (fun_image (ordinal_interval y x) f)).
proof: Proof. move => /limit_ordinal_P [xp lx] lyx fincr. have ox: ordinalp x by move: (proj32_1 lyx). set A := (ordinal_interval y x). have H i: inc i A <-> y <=o i /\ i <o x by exact:(ointvP ox y i). have osA: ordinal_set (fun_image A f). move => a /funI_P [i /H [lyi lix] ->]. exact: (proj31 (fincr i (osucc i) lyi (oleS (proj32 lyi)) (lx i lix))). split. by exists y => // i lti liy; apply: (ord_sup_ub osA);apply: funI_i; apply/H. move => l /(olt_sup osA) [t /funI_P [ z /H [za zb] ->] ll]. exists z => // i ia ib; exact:(olt_leT ll (fincr z i za ia ib)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)