proposition: Lemma near_inftyS (P : set nat) : (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
proof: Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed