proposition: Lemma cvg_addrl (M : R) : M + r @[r --> +oo] --> +oo.
proof: Proof. move=> P [r [rreal rP]]; exists (r - M); split. by rewrite realB// num_real. by move=> m; rewrite ltrBlDl => /rP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)