proposition: Lemma increasing_sup_limit2 X: ofg_Mlt_lto X -> limit_ordinal (domain X) -> limit_ordinal (\osup (range X)).
proof: Proof. move => pa pb. have p9:=(ofg_Mlt_lto_p3 pa pb). move: (p9) => [xa xb xc]. have osx:= (ofg_Mle_leo_os xa xb). have ned: nonempty (domain X) by move: pb => [_ ok _]; ex_tac. apply: (increasing_sup_limit1 p9 ned). move: pa pb => [q1 q2 q3] [qa qb qc]. move => t td bad. have lt1:= (oltS (Os_ordinal qa td)). move: (qc _ td) => sb. move: (q3 _ _ td sb lt1) => lt2. have vr: inc (Vg X (osucc t)) (range X) by apply /(range_gP q1); ex_tac. by move: (ord_sup_ub osx vr); rewrite - bad =>/(oltNge lt2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)