How to prove that every real number is bounded above by some natural number?

Using Coq
1 
Theorem test (a: R): exists k, a < INR k.

Is there a simple way to prove this theorem? I tried searching standard library, but probably missed something.

Thanks in advance.

2

Take a look at the archimed statement:

archimed: forall r : R, (IZR (up r) > r)%R /\ (IZR (up r) - r <= 1)%R

So, it is not exactly what you are looking, since it is gives you a value of type Z rather than nat. But it should not be too hard to convert it, e.g., using Z.abs_nat, and prove your theorem.

1 Like