proposition: Lemma ncvgN u lu : ncvg u lu -> ncvg (- u) (- lu).
proof: Proof. case: lu => [lu||] cu /=; first last. + elim/nbh_pinfW=> M; case: (cu (NNInf (-M))) => K {}cu. by exists K => n /cu; rewrite !inE ltrNr. + elim/nbh_ninfW=> M; case: (cu (NPInf (-M))) => K {}cu. by exists K => n /cu; rewrite !inE ltrNl. elim/nbh_finW => e /= gt0_e; case: (cu (B lu e)). by move=> K {}cu; exists K=> n /cu; rewrite !inE -opprD normrN eclamp_id. 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