I can write

```
Variable R : realType.
Lemma near_in_interval (a b : R) :
{in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}.
```

but in the same context, I can't write

```
Lemma near_0_in_interval (a b : R) :
{in `]a, b[, forall y, \forall z \near 0, (z + y : R) \in `]a, b[}.
```

Is there a simple type annotation to add so that it works?

I guess it does not know the type of 0

Did you open `ring_scope`

?

or try (0 : R)

Thanks Laurent, your hint does the trick.

And thanks Kazuhiko, but ring_scope was already open.

Last updated: Jun 25 2024 at 18:02 UTC