proposition: Lemma cvg_arithmetic (R : archiFieldType) a (z : R) : z > 0 -> arithmetic a z @ \oo --> +oo.
proof: Proof. move=> z_gt0; apply/cvgryPge => A; near=> n => /=. rewrite -lerBlDl -mulr_natl -ler_pdivrMr//. rewrite ler_normlW// ltW// (lt_le_trans (archi_boundP _))// ler_nat. by near: n; apply: nbhs_infty_ge. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau