proposition: Lemma cvg_subnr N : subn^~ N @ \oo --> \oo.
proof: Proof. move=> P [n _ Pn]; exists (N + n)%N => //= m le_m. by apply: Pn; rewrite /= leq_subRL// (leq_trans _ le_m)// leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed