proposition: Lemma cvg_addrr (M : R) : (r + M) @[r --> +oo] --> +oo.
proof: Proof. by under [X in X @ _]funext => n do rewrite addrC; exact: cvg_addrl. 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)