proposition: Lemma ncvg_homo_lt (u : nat -> R) (l1 l2 : \bar R) : (forall m n, (m <= n)%N -> u m <= u n) -> (l1 < l2)%E -> ncvg u l1 -> forall n, ((u n)%:E < l2)%E.
proof: Proof. move=> homo_u lt_12 cvu n; have [K {cvu}cv] := ncvg_lt lt_12 cvu. case: (leqP n K) => [/homo_u|/ltnW /cv //]. by move/lee_tofin/le_lt_trans; apply; apply/cv. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology