```
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.

```
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.

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