proposition: Lemma cvg_harmonic {R : archiFieldType} : @harmonic R @ \oo --> 0.
proof: Proof. apply/cvgrPdist_le => _/posnumP[e]; near=> i. rewrite distrC subr0 ger0_norm//= -lef_pV2 ?qualifE//= invrK. rewrite (le_trans (ltW (archi_boundP _)))// ler_nat -add1n -leq_subLR. by near: i; 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