Missing lemma `cvg_addrl_Ny`

[hoheinzollern]

Lemma cvg_addrl_Ny (M : R) : M + r @[r --> -oo] --> -oo.
Proof.
move=> P [r [rreal rP]]; exists (r - M); split.
  by rewrite realB// num_real.
by move=> m/=; rewrite ltrBrDl => /rP.
Qed.