proposition: Lemma inverses_of_nats_approach_0: forall eps:R, eps > 0 -> exists n:nat, (n > 0)%nat /\ / (INR n) < eps.
proof: Proof. intros. assert (exists n:Z, (n>0)%Z /\ / (IZR n) < eps). { exists (up (/ eps)). split. - assert (IZR (up (/ eps)) > 0). { eapply Rgt_trans; auto with real rorders. } apply lt_0_IZR in H0. now apply Z.lt_gt. - pattern eps at 2. rewrite <- Rinv_involutive; auto with real; apply Rinv_lt_contravar; auto with real; apply Rmult_lt_0_compat; auto with real; apply Rlt_trans with (/ eps); auto with real. } destruct H0 as [[ | p | p ]]; destruct H0; try inversion H0. exists (nat_of_P p). unfold IZR in H1. rewrite <- INR_IPR in H1. auto with real. Qed.
imports: Reals Qreals Lra