proposition: Lemma ncvg_gt (u : nat -> R) (l1 l2 : \bar R) : (l1 < l2)%E -> ncvg u l2 -> exists K, forall n, (K <= n)%N -> (l1 < (u n)%:E)%E.
proof: Proof. case: l1 l2 => [l1||] [l2||] //=; first last. + by move=> _ _; exists 0%N => ? ?; exact: ltNyr. + by move=> _ _; exists 0%N => ? ?; exact: ltNyr. + by move=> _ /(_ (NPInf l1)) [K cv]; exists K => n /cv. move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)). case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //. rewrite ltr_distl => /andP[] /(le_lt_trans _) h _; apply: h. by rewrite {cv}/e opprB addrCA subrr addr0. 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