proposition: Lemma olim_sup f x: limit_ordinal x -> (forall i j, i <=o j -> j <o x -> f i <=o f j) -> olimit f x (\osup (fun_image x f)).
proof: Proof. move => lx ha. move/limit_ordinal_P: (lx) => [xp _]. have hb: (forall i j, \0o <=o i -> i <=o j -> j <o x -> f i <=o f j). move => i j _; apply: ha. by move:(olim_sup_spec lx xp hb); rewrite (ointv_pr1 (proj32_1 xp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)