proposition: Lemma INR_archimed : forall eps A : R, eps > 0 -> exists n : nat, (INR n) * eps > A.
proof: Proof. intros eps A Heps; destruct (INR_unbounded (A / eps)) as [N HN]. exists N. apply (Rmult_gt_reg_r (/ eps)). { now apply Rinv_0_lt_compat. } now rewrite Rmult_assoc, Rinv_r by (now apply Rgt_not_eq); rewrite Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField