proposition: Lemma cvg_divnr N : (N > 0)%N -> divn^~ N @ \oo --> \oo.
proof: Proof. move=> N_gt0 P [n _ Pn]; exists (n * N)%N => //= m. by rewrite /= -leq_divRL//; apply: Pn. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed