proposition: Lemma INR_unbounded : forall A, exists n, INR n > A.
proof: Proof. intros A; destruct (Rle_or_lt 0 A) as [A_ge0 | A_lt0]; cycle 1. { now exists 0%nat; simpl. } destruct (archimed A) as [ar1 _]. exists (Z.to_nat (up A)). rewrite INR_IZR_INZ, Z2Nat.id; try assumption. apply le_IZR, Rle_trans with (1 := A_ge0). now left. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField