proposition: Lemma ncvg_le v u (lv lu : \bar R) : u <=1 v -> ncvg v lv -> ncvg u lu -> (lu <= lv)%E.
proof: Proof. by move=> le_uv; apply/(@ncvg_le_from 0). 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