proposition: Lemma ncvg_le_from K v u (lv lu : \bar R) : (forall n, (K <= n)%N -> u n <= v n) -> ncvg v lv -> ncvg u lu -> (lu <= lv)%E.
proof: Proof. move=> le_uv cv cu; rewrite leNgt; apply/negP=> /separable_le. case=> [v1] [v2] h; have [] := (cv v1, cu v2). case=> [K1 vv1] [K2 uv2]; pose_big_enough K'. have []// := And3 (le_uv K' _) (vv1 K' _) (uv2 K' _). 2: by close. by move=> le h1 h2; have := h _ _ h1 h2; rewrite ltNge le. 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