proposition: Lemma osi_gex1 x f: sincr_ofs f -> ordinalp x -> exists y, [/\ ordinalp y, x <=o (f y) & forall z, ordinalp z -> x <=o (f z) -> y <=o z].
proof: Proof. move=> finc ox. have lxy:= (osi_gex finc ox). pose p y := x <=o (f y). have [pa pb pc]:= (@least_ordinal4 x p ox lxy). by exists (least_ordinal p x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)