proposition: Lemma increasing_sup_limit1 X (a:= \osup (range X)): ofg_Mle_leo X -> nonempty (domain X) -> (allf X (fun t => t <> a)) -> limit_ordinal a.
proof: Proof. move=> [fgX pb pc] [x xd] pd. move: (ofg_Mle_leo_os fgX pb) => osx. have ner: nonempty (range X) by exists (Vg X x); apply /(range_gP fgX); ex_tac. case: (ord_sup_inVlimit osx ner) => //. by rewrite -/a; aw; move /(range_gP fgX)=> [t td av]; case: (pd _ td). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)