proposition: Lemma osi_gexu f u t x: sincr_ofsu f u -> u <=o t -> t <=o f t -> t <=o x -> x <=o (f x).
proof: Proof. move=> finc ut tft tx. have ox:=proj32 tx. move: x ox tx; apply: least_ordinal2 => x ox xp ltx. case: (oleT_el ox (ofs_sincru finc (oleT ut ltx))) => // lt1. case:(ole_eqVlt ltx) => ty; first ue. have pa:=(oleT tft (proj1 (finc t x ut ty))). case: (oltNge (finc (f x) x (oleT ut pa) lt1) (xp _ lt1 pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)