proposition: Lemma osi_gex x f: sincr_ofs f -> ordinalp x -> x <=o (f x).
proof: Proof. move=> finc; move: x; apply: least_ordinal2 => x ox xp. case: (oleT_el ox (ofs_sincr finc ox)) => // lt1. case: (oleNgt (xp _ lt1) (finc _ _ lt1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)